Use context in PCUICAst.mutual_inductive_entry

MetaCoq · Nov 29, 2022 · 380690d · 380690d
1 parent c9f5878
commit 380690d
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 4 deletions.
diff --git a/pcuic/theories/PCUICAst.v b/pcuic/theories/PCUICAst.v
@@ -1309,7 +1309,7 @@ Record mutual_inductive_entry := {
      If so, is it primitive, using binder name [ident]
      for the record in primitive projections ? *)
   mind_entry_finite    : recursivity_kind;
-  mind_entry_params    : list (ident * local_entry);
+  mind_entry_params    : context;
   mind_entry_inds      : list one_inductive_entry;
   mind_entry_universes : universes_decl;
   mind_entry_private   : option bool

diff --git a/pcuic/theories/utils/PCUICAstUtils.v b/pcuic/theories/utils/PCUICAstUtils.v
@@ -233,9 +233,7 @@ Proof.
     destruct typ as [[names types] _].
     apply (List.firstn decl.(ind_npars)) in names.
     apply (List.firstn decl.(ind_npars)) in types.
-    refine (List.combine _ _).
-    exact (List.map string_of_aname names).
-    exact (List.map LocalAssum types).
+    refine (map (fun '(x, ty) => vass x ty) (combine names types)).
   - refine (List.map _ decl.(ind_bodies)).
     intros [].
     refine {| mind_entry_typename := ind_name0;