do not unfold letins in instances

Author: gares

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]
 ].