changing mk-phant-abbrev to use skeletons

Author: CohenCyril

hb.elpi

@@ -946,9 +946,9 @@ mk-phant-abbrev.term K F [unify-arg|AL] K' FAbbrev :- !,
   mk-phant-abbrev.term K {mk-app F [{{lib:@hb.id _ _}}]} AL K' FAbbrev.
 
 pred mk-phant-abbrev i:string, i:phant-term, o:constant, o:abbreviation.
-mk-phant-abbrev N (phant-term AL T) C Abbrev :- std.do! [
+mk-phant-abbrev N (phant-term AL T1) C Abbrev :- std.do! [
   NC is "phant_" ^ N,
-  std.assert-ok! (coq.typecheck T TTy) "mk-phant-abbrev: T illtyped",
+  std.assert-ok! (coq.elaborate-skeleton T1 TTy T) "mk-phant-abbrev: T illtyped",
   hb-add-const NC T TTy @transparent! C,
   mk-phant-abbrev.term 0 (global (const C)) AL NParams AbbrevT,
   @global! => coq.notation.add-abbreviation N NParams AbbrevT tt Abbrev,
@@ -1657,20 +1657,21 @@ pack-body ClassName PL T MLwA F :- std.do! [
 
 pred declare-auto-infer-params-abbrev i:structure, i:list-w-params mixinname.
 declare-auto-infer-params-abbrev GR MLwP :- get-option "infer" Map, !,
-  Map => mk-infer (global GR) MLwP PHARGS TSK,
-  std.assert-ok! (coq.elaborate-skeleton TSK _ T) "infer illtyped",
-  mk-phant-abbrev "type" (phant-term PHARGS T) _ _.
+  Map => mk-infer (global GR) MLwP PHT,
+  mk-phant-abbrev "type" PHT _ _.
 declare-auto-infer-params-abbrev _ _.
 
-pred mk-infer i:term, i:list-w-params mixinname, o:list phant-arg, o:term.
-mk-infer T (w-params.nil _ _ _) [] T.
-mk-infer T (w-params.cons N Ty W) [implicit-arg, infer-type N|A] R1 :- coq.name->id N ID, (get-option ID "Type" ; get-option ID ""), !,
+pred mk-infer i:term, i:list-w-params mixinname, o:phant-term.
+mk-infer T (w-params.nil _ _ _) (phant-term [] T).
+mk-infer T (w-params.cons N Ty W) (phant-term [implicit-arg, infer-type N|A] R1) :-
+  coq.name->id N ID, (get-option ID "Type" ; get-option ID ""), !,
   R1 = (fun N Ty n\ fun `ph` {{ lib:@hb.phant lp:n }} _\ R n),
   @pi-decl N Ty n\
-    mk-infer {mk-app T [n]} (W n) A (R n).
-mk-infer T (w-params.cons N Ty W) [real-arg N|A] (fun N Ty R) :- coq.name->id N ID, not (get-option ID _), !,
-  @pi-decl N Ty x\  mk-infer {mk-app T [x]} (W x) A (R x).
-mk-infer _ (w-params.cons N _ _) _ _ :- coq.name->id N ID, get-option ID Infer,
+    mk-infer {mk-app T [n]} (W n) (phant-term A (R n)).
+mk-infer T (w-params.cons N Ty W) (phant-term [real-arg N|A] (fun N Ty R)) :-
+   coq.name->id N ID, not (get-option ID _), !,
+  @pi-decl N Ty x\  mk-infer {mk-app T [x]} (W x) (phant-term A (R x)).
+mk-infer _ (w-params.cons N _ _) _ :- coq.name->id N ID, get-option ID Infer,
   coq.error "Automatic inference of paramter" N "from" Infer "not supported".
 
 % HB.structure Definition S P1 P2 := { T of F1 P1 T & F2 P1 (P2*P2) T }