diff --git a/pcuic/theories/PCUICAst.v b/pcuic/theories/PCUICAst.v
index 0a79cb462..f2e4f3c72 100644
--- 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
index d67b0be8d..8036b90fe 100644
--- 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;