port to coq-elpi 1.4

hb.elpi

@@ -125,14 +125,16 @@ name-of-asset-decl (asset-record X _ _ _) X.
 name-of-asset-decl (asset-alias X _) X.
 
 pred argument->asset i:argument, o:asset-decl.
-argument->asset (indt-decl (parameter Name Ty I)) (asset-parameter "T" Ty A) :- % TODO, take the name
+argument->asset (indt-decl (parameter ID _ Ty I)) (asset-parameter ID Ty A) :-
+  coq.string->name ID Name,
   @pi-decl Name Ty a\
     argument->asset (indt-decl (I a)) (A a).
 argument->asset (indt-decl (record Rid Ty Kid F)) (asset-record Rid Ty Kid F) :- !.
-argument->asset (const-decl Id (some (fun _ _ Bo)) (some (prod Name Src Ty))) (asset-parameter "T" Src A) :- !,
+argument->asset (const-decl Id (some (fun _ _ Bo)) (parameter ID _ Src Ty)) (asset-parameter ID Src A) :- !,
+  coq.id->name ID Name,
   @pi-decl Name Src a\
-    argument->asset (const-decl Id (some (Bo a)) (some (Ty a))) (A a).
-argument->asset (const-decl Id (some Bo) (some Ty)) (asset-alias Id Bo) :- !,
+    argument->asset (const-decl Id (some (Bo a)) (Ty a)) (A a).
+argument->asset (const-decl Id (some Bo) (arity Ty)) (asset-alias Id Bo) :- !,
   std.assert! (var Ty) "Factories aliases should not be given a type".
 argument->asset X _ :- coq.error "Unsupported asset:" X.
 
@@ -966,7 +968,7 @@ declare-class ML (indt ClassName) Factories :- std.do! [
 
   (@pi-decl `T` {{Type}} t\ synthesize-fields t ML (RDecl t)),
   ClassDeclaration =
-    (parameter `T` {{ Type }} t\
+    (parameter "T" explicit {{ Type }} t\
       record "axioms" {{ Type }} "Class" (RDecl t)),
   std.assert-ok! (coq.typecheck-indt-decl ClassDeclaration) "declare-class: illtyped",
   coq.env.add-indt ClassDeclaration ClassName,
@@ -1149,11 +1151,11 @@ declare-old-constant (some C) :-
 declare-old-constant _ :- true.
 
 pred main-begin-declare-builders i:context-decl.
-main-begin-declare-builders (context-item _ _ none _\ context-item IDF _ (some _) _\ context-end) :-
+main-begin-declare-builders (context-item _ _ _ none _\ context-item IDF _ _ (some _) _\ context-end) :-
     coq.error "factories cannot be given a body:" IDF.
-main-begin-declare-builders (context-item _ _ none _\ context-item ID1 _ none _\ context-item ID2 _ _ _) :-
+main-begin-declare-builders (context-item _ _ _ none _\ context-item ID1 _ _ none _\ context-item ID2 _ _ _ _) :-
   coq.error "only one factory is supported, got at least two" ID1 "and" ID2.
-main-begin-declare-builders (context-item IDT T none t\ context-item IDF (F t) none _\ context-end) :- std.do! [
+main-begin-declare-builders (context-item IDT _ T none t\ context-item IDF _ (F t) none _\ context-end) :- std.do! [
   Name is "Builders_" ^ {term_to_string {new_int}}, % TODO
   std.assert! (pi t\ F t = app[global GRA, t|_]) "a factory must be a name applied to the type variable",
   factory-alias->gref GRA GRF,