Remove check_hidden_implicit_parameters (not needed anymore)

4 files changed, 13 insertions, 33 deletions

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 9a69af0f64..905d9f1e5b 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -48,7 +48,7 @@ open NumTok
    types and recursive definitions and of projection names in records *)
 
 type var_internalization_type =
-  | Inductive of Id.t list (* list of params *) * bool (* true = check for possible capture *)
+  | Inductive
   | Recursive
   | Method
   | Variable
@@ -415,20 +415,6 @@ let locate_if_hole ?loc na c = match DAst.get c with
       with Not_found -> DAst.make ?loc @@ GHole (Evar_kinds.BinderType na, naming, arg))
   | _ -> c
 
-let reset_hidden_inductive_implicit_test env =
-  { env with impls = Id.Map.map (function
-         | (Inductive (params,_),b,c) -> (Inductive (params,false),b,c)
-         | x -> x) env.impls }
-
-let check_hidden_implicit_parameters ?loc id impls =
-  if Id.Map.exists (fun _ -> function
-    | (Inductive (indparams,check),_,_) when check -> Id.List.mem id indparams
-    | _ -> false) impls
-  then
-    user_err ?loc (Id.print id ++ strbrk " is already used as name of " ++
-      strbrk "a parameter of the inductive type; bound variables in " ++
-      strbrk "the type of a constructor shall use a different name.")
-
 let pure_push_name_env (id,implargs) env =
   {env with
     ids = Id.Set.add id env.ids;
@@ -442,7 +428,6 @@ let push_name_env ntnvars implargs env =
   | { loc; v = Anonymous } ->
       env
   | { loc; v = Name id } ->
-      check_hidden_implicit_parameters ?loc id env.impls ;
       if Id.Map.is_empty ntnvars && Id.equal id ldots_var
         then error_ldots_var ?loc;
       set_var_scope ?loc id false (env.tmp_scope,env.scopes) ntnvars;
@@ -895,9 +880,6 @@ let instantiate_notation_constr loc intern intern_pat ntnvars subst infos c =
     try
       let pat,(onlyident,scopes) = Id.Map.find id binders in
       let env = set_env_scopes env scopes in
-      (* We deactivate impls to avoid the check on hidden parameters *)
-      (* and since we are only interested in the pattern as a term *)
-      let env = reset_hidden_inductive_implicit_test env in
       if onlyident then
         term_of_name (out_patvar pat)
       else
@@ -1001,7 +983,7 @@ let intern_notation intern env ntnvars loc ntn fullargs =
 (* Discriminating between bound variables and global references       *)
 
 let string_of_ty = function
-  | Inductive _ -> "ind"
+  | Inductive -> "ind"
   | Recursive -> "def"
   | Method -> "meth"
   | Variable -> "var"
@@ -2104,7 +2086,8 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
         let env' = Id.Set.fold
           (fun var bli -> push_name_env ntnvars (Variable,[],[]) bli (CAst.make @@ Name var))
           (Id.Set.union ex_ids as_in_vars)
-          (reset_hidden_inductive_implicit_test (restart_lambda_binders env)) in
+          (restart_lambda_binders env)
+        in
         (* PatVars before a real pattern do not need to be matched *)
         let stripped_match_from_in =
           let rec aux = function
@@ -2139,17 +2122,17 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
         (* "in" is None so no match to add *)
         let ((b',(na',_)),_,_) = intern_case_item env' Id.Set.empty (b,na,None) in
         let p' = Option.map (fun u ->
-          let env'' = push_name_env ntnvars (Variable,[],[]) (reset_hidden_inductive_implicit_test env')
+          let env'' = push_name_env ntnvars (Variable,[],[]) env'
             (CAst.make na') in
           intern_type (slide_binders env'') u) po in
         DAst.make ?loc @@
         GLetTuple (List.map (fun { CAst.v } -> v) nal, (na', p'), b',
-                   intern (List.fold_left (push_name_env ntnvars (Variable,[],[])) (reset_hidden_inductive_implicit_test env) nal) c)
+                   intern (List.fold_left (push_name_env ntnvars (Variable,[],[])) env nal) c)
     | CIf (c, (na,po), b1, b2) ->
       let env' = reset_tmp_scope env in
       let ((c',(na',_)),_,_) = intern_case_item env' Id.Set.empty (c,na,None) in (* no "in" no match to ad too *)
       let p' = Option.map (fun p ->
-          let env'' = push_name_env ntnvars (Variable,[],[]) (reset_hidden_inductive_implicit_test env)
+          let env'' = push_name_env ntnvars (Variable,[],[]) env
             (CAst.make na') in
           intern_type (slide_binders env'') p) po in
         DAst.make ?loc @@
diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index fb1c6684a1..9f06f16258 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -38,7 +38,7 @@ open Pretyping
    of [env] *)
 
 type var_internalization_type =
-  | Inductive of Id.t list (* list of params *) * bool (* true = check for possible capture *)
+  | Inductive
   | Recursive
   | Method
   | Variable
diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml
index 895561324b..458714403a 100644
--- a/vernac/comInductive.ml
+++ b/vernac/comInductive.ml
@@ -503,8 +503,8 @@ let interp_mutual_inductive_gen env0 ~template udecl (uparamsl,paramsl,indl) not
 
   (* Compute interpretation metadatas *)
   let indimpls = List.map (fun impls -> userimpls @ impls) indimpls in
-  let impls = compute_internalization_env env_uparams sigma ~impls (Inductive (params,true)) indnames fullarities indimpls in
-  let ntn_impls = compute_internalization_env env_uparams sigma (Inductive (params,true)) indnames fullarities indimpls in
+  let impls = compute_internalization_env env_uparams sigma ~impls Inductive indnames fullarities indimpls in
+  let ntn_impls = compute_internalization_env env_uparams sigma Inductive indnames fullarities indimpls in
 
   let ninds = List.length indl in
   let (sigma, _), constructors =
diff --git a/vernac/record.ml b/vernac/record.ml
index 785ed89372..b9d450044b 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -114,7 +114,7 @@ let check_anonymous_type ind =
   | { CAst.v = CSort (Glob_term.UAnonymous {rigid=true}) } -> true
   | _ -> false
 
-let typecheck_params_and_fields finite def poly pl ps records =
+let typecheck_params_and_fields def poly pl ps records =
   let env0 = Global.env () in
   (* Special case elaboration for template-polymorphic inductives,
      lower bound on introduced universes is Prop so that we do not miss
@@ -168,13 +168,10 @@ let typecheck_params_and_fields finite def poly pl ps records =
   let fold accu (id, _, _, _) arity r =
     EConstr.push_rel (LocalAssum (make_annot (Name id) r,arity)) accu in
   let env_ar = EConstr.push_rel_context newps (List.fold_left3 fold env0 records arities relevances) in
-  let assums = List.filter is_local_assum newps in
   let impls_env =
-    let params = List.map (RelDecl.get_name %> Name.get_id) assums in
-    let ty = Inductive (params, (finite != Declarations.BiFinite)) in
     let ids = List.map (fun (id, _, _, _) -> id) records in
     let imps = List.map (fun _ -> imps) arities in
-    compute_internalization_env env0 sigma ~impls:impls_env ty ids arities imps
+    compute_internalization_env env0 sigma ~impls:impls_env Inductive ids arities imps
   in
   let ninds = List.length arities in
   let nparams = List.length newps in
@@ -714,7 +711,7 @@ let definition_structure udecl kind ~template ~cumulative ~poly finite records =
   let ps, data = extract_record_data records in
   let ubinders, univs, auto_template, params, implpars, data =
     States.with_state_protection (fun () ->
-      typecheck_params_and_fields finite (kind = Class true) poly udecl ps data) () in
+      typecheck_params_and_fields (kind = Class true) poly udecl ps data) () in
   let template = template, auto_template in
   match kind with
   | Class def ->