Merge PR #8684: Remove a few circumvolutions around parameters of inductive entries

2 files changed, 2 insertions, 14 deletions

diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml
index 885a22b209..5ff3032ec4 100644
--- a/vernac/comInductive.ml
+++ b/vernac/comInductive.ml
@@ -102,10 +102,6 @@ let mk_mltype_data sigma env assums arity indname =
   let is_ml_type = is_sort env sigma arity in
   (is_ml_type,indname,assums)
 
-let prepare_param = function
-  | LocalAssum (na,t) -> Name.get_id na, LocalAssumEntry t
-  | LocalDef (na,b,_) -> Name.get_id na, LocalDefEntry b
-
 (** Make the arity conclusion flexible to avoid generating an upper bound universe now,
     only if the universe does not appear anywhere else.
     This is really a hack to stay compatible with the semantics of template polymorphic
@@ -463,7 +459,7 @@ let interp_mutual_inductive_gen env0 ~template udecl (uparamsl,paramsl,indl) not
   in
   (* Build the mutual inductive entry *)
   let mind_ent =
-    { mind_entry_params = List.map prepare_param ctx_params;
+    { mind_entry_params = ctx_params;
       mind_entry_record = None;
       mind_entry_finite = finite;
       mind_entry_inds = entries;
diff --git a/vernac/record.ml b/vernac/record.ml
index 3ba360fee4..7a4c38e972 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -191,14 +191,6 @@ let typecheck_params_and_fields finite def poly pl ps records =
   let ans = List.map2 map data typs in
   ubinders, univs, template, newps, imps, ans
 
-let degenerate_decl decl =
-  let id = match RelDecl.get_name decl with
-    | Name id -> id
-    | Anonymous -> anomaly (Pp.str "Unnamed record variable.") in
-  match decl with
-    | LocalAssum (_,t) -> (id, LocalAssumEntry t)
-    | LocalDef (_,b,_) -> (id, LocalDefEntry b)
-
 type record_error =
   | MissingProj of Id.t * Id.t list
   | BadTypedProj of Id.t * env * Type_errors.type_error
@@ -437,7 +429,7 @@ let declare_structure finite ubinders univs paramimpls params template ?(kind=St
   in
   let blocks = List.mapi mk_block record_data in
   let mie =
-    { mind_entry_params = List.map degenerate_decl params;
+    { mind_entry_params = params;
       mind_entry_record = Some (if !primitive_flag then Some binder_name else None);
       mind_entry_finite = finite;
       mind_entry_inds = blocks;