fix bug

hb.elpi

@@ -1783,11 +1783,11 @@ main-begin-declare-builders CtxSkel :- std.do! [
   builders-postulate-factories CtxSkel,
 ].
 
-pred postulate-factory-abbrev i:term, i:id, i:factoryname, o:term.
-postulate-factory-abbrev TheType Name Falias TheFactory :- std.do! [
+pred postulate-factory-abbrev i:term, i:list term, i:id, i:factoryname, o:term.
+postulate-factory-abbrev TheType Params Name Falias TheFactory :- std.do! [
   factory-alias->gref Falias F,
   phant-abbrev F _ Fabv,
-  coq.notation.abbreviation Fabv [TheType] Package, % BUG
+  coq.notation.abbreviation Fabv {std.append Params [TheType]} Package,
   Msg is "Unable to declare factory " ^ Name,
   std.assert-ok! (coq.typecheck-ty Package _) Msg,
   @local! => hb-add-const Name _ Package @opaque! C,
@@ -1832,7 +1832,7 @@ builders-postulate-factories (context-item IDT _ TySkel none t\ context-item IDF
     "the last argument must be a factory applied to the type variable",
   factory-requires GRF GRFMLwP, % TODO: remove, pass to main-declare-context the list-w-params-eta-expansion of GRF
   main-declare-context TheType Params GRFMLwP _,
-  postulate-factory-abbrev TheType IDF GRF TheFactory,
+  postulate-factory-abbrev TheType Params IDF GRF TheFactory,
   define-factory-operations TheType TheFactory GRF,
   acc current (clause _ _ (current-decl (builders-for-factory GRF))),
 ].