fix elaboration of parameters in HB.structure

Author: gares

hb.elpi

@@ -116,6 +116,10 @@ located->gref S [loc-modpath _|_] _ :- coq.error S "should be a factory, but is
 located->gref S [loc-modtypath _|_] _ :- coq.error S "should be a factory, but is a module type".
 located->gref S [] _ :- coq.error "Could not locate name" S.
 
+pred purge-id i:term, o:term.
+purge-id T T1 :-
+  (pi fresh t v\ copy {{lib:@hb.id lp:t lp:v}} fresh :- !) => copy T T1.
+
 % TODO: generalize/rename when we support parameters
 pred argument->gref i:argument, o:gref.
 argument->gref (str S) GR :- located->gref S {coq.locate-all S} GR.

structures.v

@@ -290,7 +290,8 @@ sigT->list-w-params {{ lib:@hb.sigT _ lp:{{ fun N Ty B }} }} L C :-
     product->triples (B t) (Rest t) C.
 
 main [const-decl Module (some B) _] :- !, std.do! [
-  sigT->list-w-params B GRFS ClosureCheck, !,
+  purge-id B B1, std.assert-ok! (coq.elaborate-skeleton B1 _ B2) "illtyped structure definition",
+  sigT->list-w-params B2 GRFS ClosureCheck, !,
   with-attributes (main-declare-structure Module GRFS ClosureCheck),
 ].
 main _ :- coq.error "Usage: HB.structure Definition <ModuleName> := { A of <Factory1> A & … & <FactoryN> A }".