Merge pull request #276 from math-comp/faster-hb-pack

do not unfold letins in instances

Author: CohenCyril

.nix/config.nix

@@ -12,7 +12,7 @@
       mathcomp-single-planB.job = true;
       graph-theory.job = false;
       fourcolor.override.version = "master";
-      odd-order.override.version = "master";
+      odd-order.override.version = "hirarchy-builder";
       mathcomp-finmap.override.version = "#84";
     };
   in {

HB/pack.elpi

@@ -43,12 +43,12 @@ synth-instance Params KC KS T Tkey [Factory|Factories] Instance :-
 synth-instance Params KC KS T Tkey [] Instance :- coq.safe-dest-app Tkey (global _) _, !,
   synthesis.under-local-canonical-mixins-of.do! Tkey [
     std.assert-ok! (synthesis.infer-all-args-let Params Tkey KC ClassInstance) "HB.pack: cannot infer the instance",
-    std.append Params [T, {unwind {hd-beta-zeta ClassInstance []}}] InstanceArgs,
+    std.append Params [T, ClassInstance] InstanceArgs,
       Instance = app[global KS | InstanceArgs]
 ].
 synth-instance Params KC KS T Tkey [] Instance :- std.do! [
   std.assert-ok! (synthesis.infer-all-args-let Params Tkey KC ClassInstance) "HB.pack: cannot infer the instance",
-  std.append Params [T, {unwind {hd-beta-zeta ClassInstance []}}] InstanceArgs,
+  std.append Params [T, ClassInstance] InstanceArgs,
     Instance = app[global KS | InstanceArgs]
 ].