speedup: do not use grafting :before, currently inefficient

Author: gares

HB/common/synthesis.elpi

@@ -191,10 +191,16 @@ mixin-for T M MICompressed :- mixin-src T M Tm, !, std.do! [
   compress-coercion-paths MI MICompressed,
 ].
 
+pred compress-copy o:term, o:term.
+compress-copy X Y :- compress X Y, !.
+compress-copy (app L) (app L1) :- !, std.map L compress-copy L1.
+compress-copy X X.
+
+
 pred compress-coercion-paths i:term, o:term.
 compress-coercion-paths MI MICompressed :-
   if (get-option "compress_coercions" tt)
-     (compress MI MICompressed)
+     (compress-copy MI MICompressed)
      (MI = MICompressed).
 
 pred mixin-for_mixin-builder i:prop, o:term.

HB/structure.elpi

@@ -398,7 +398,7 @@ declare-coercion SortProjection ClassProjection
   std.map AllTgtSuper class_structure AllTgtSuperStructures,
 
   mk-compression-clauses StructureF StructureT AllTgtSuperStructures AllCompressionClauses,
-  std.forall AllCompressionClauses (c\ log.coq.env.accumulate current "hb.db" (clause _ (before "compress:begin") c)),
+  std.forall AllCompressionClauses (c\ log.coq.env.accumulate current "hb.db" (clause _ _ c)),
 ].
 
 

structures.v

@@ -232,9 +232,6 @@ pred docstring o:loc, o:string.
 % terms, since this is what you get when you apply coercions)
 :index (4)
 pred compress o:term, o:term.
-:name "compress:begin"
-compress (app L) (app L1) :- !, std.map L compress L1.
-compress X X.
 
 }}.