Merge pull request #569 from LPCIC/fix-imp-record

fix: HOAS impargs of record

Author: gares

src/coq_elpi_HOAS.ml

@@ -2972,7 +2972,7 @@ let lp2inductive_entry ~depth coq_ctx constraints state t =
         let state, fields_names_coercions, kty = aux_fields (depth+1) state ind fields in
         let k = [E.mkApp constructorc kn [in_elpi_arity kty]] in
         let state, idecl, uctx, ubinders, i_impls, ks_impls, gl2 =
-          aux_construtors (push_coq_ctx_local depth e coq_ctx) ~depth:(depth+1) (params,impls) ([],[]) arity iname Declarations.BiFinite
+          aux_construtors (push_coq_ctx_local depth e coq_ctx) ~depth:(depth+1) (params,List.rev impls) ([],[]) arity iname Declarations.BiFinite
             state k in
         let primitive = coq_ctx.options.primitive = Some true in
         state, (idecl, uctx, ubinders, Some (primitive,fields_names_coercions), [i_impls, ks_impls]), List.(concat (rev (gl2 :: gl1 :: extra)))

tests/test_HOAS.v

@@ -616,3 +616,11 @@ coq.env.add-indt D _,
 coq.env.end-module _
 }}.
 
+
+Elpi Command Comm.
+Elpi Accumulate  lp:{{
+  main [indt-decl X] :- coq.say X,
+    coq.env.add-indt X _.
+}}.
+Elpi Comm Class c {A : Type} (x : A -> A).
+Goal c S. Abort.