Revert "Warn about possible shadowing of a name occurring in a "in" clause."

This reverts commit 46f876a9404844487476415af2e6f6d938558d15.

1 files changed, 2 insertions, 8 deletions

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 443039b95..9304247a2 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -1287,7 +1287,7 @@ let intern_ind_pattern genv scopes pat =
       let idslpl2 = List.map (intern_pat genv empty_alias) pl2 in
       (with_letin,
        match product_of_cases_patterns [] (List.rev_append idslpl1 idslpl2) with
-       | ids,[_,pl] -> (ids,c,chop_params_pattern loc c pl with_letin)
+       | _,[_,pl] -> (c,chop_params_pattern loc c pl with_letin)
        | _ -> error_bad_inductive_type loc)
     | x -> error_bad_inductive_type (raw_cases_pattern_expr_loc x)
 
@@ -1639,13 +1639,7 @@ let internalize globalenv env allow_patvar lvar c =
     (* the "in" part *)
     let match_td,typ = match t with
     | Some t ->
-	let with_letin,(ids,ind,l) = intern_ind_pattern globalenv (None,env.scopes) t in
-        let is_shadowing id = Name.equal (snd na) (Name id) && Id.Set.mem id forbidden_names_for_gen in
-        List.iter (fun id -> if is_shadowing id then
-          msg_warning
-            (str "Name " ++ pr_id id ++
-             strbrk " on which pattern-matching is done is shadowing the binder of same name in its \"in\" clause."))
-          ids;
+	let with_letin,(ind,l) = intern_ind_pattern globalenv (None,env.scopes) t in
 	let (mib,mip) = Inductive.lookup_mind_specif globalenv ind in
 	let nparams = (List.length (mib.Declarations.mind_params_ctxt)) in
 	(* for "in Vect n", we answer (["n","n"],[(loc,"n")])