cleanup

Author: gares

HB/instance.elpi

@@ -402,7 +402,7 @@ declare-wrapper-inst TheType ML TheMixins TyWP SectionName CSL :- std.do![
 
 pred is-structure-op-w-wrapper i:term.
 is-structure-op-w-wrapper (global (const C)) :- exported-op _ _ C, wrapper-mixin _ (const C) _.
-is-structure-op-w-wrapper (app[global (const C)|_]) :- std.spy(exported-op _ _ C), wrapper-mixin _ (const C) _.
+is-structure-op-w-wrapper (app[global (const C)|_]) :- exported-op _ _ C, wrapper-mixin _ (const C) _.
 
 pred derive-wrapper-instances i:term, i:mixinname, o:term, o:constant.
 derive-wrapper-instances Instance WrapperMixin WrapperSubject C :- std.do! [
@@ -440,7 +440,7 @@ derive-wrapper-instances Instance WrapperMixin WrapperSubject C :- std.do! [
 
     Name is "wrapped__" ^ {std.any->string {new_int}},
 
-    std.spy(log.coq.env.add-const-noimplicits Name NewInstance Ty @transparent! C),
+    log.coq.env.add-const-noimplicits Name NewInstance Ty @transparent! C,
   ].
 
 pred wrap-a-mixin i:gref, i:mixinname, i:constant, o:term, o:mixinname, o:constant.

tests/monoid_enriched_cat.v

@@ -62,7 +62,7 @@ Succeed HB.structure
               (forall A B : Obj, isMon (hom A B)) }.
 
                           (* which one is best? *)
-Fail HB.structure
+Succeed HB.structure
   Definition Monoid_enriched_quiver :=
     { Obj of isQuiver Obj &
             (forall A B : Obj, isMon (@hom (Quiver.clone Obj _) A B)) }.