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

1 files changed, 8 insertions, 2 deletions

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 9304247a2..443039b95 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
-       | _,[_,pl] -> (c,chop_params_pattern loc c pl with_letin)
+       | ids,[_,pl] -> (ids,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,7 +1639,13 @@ let internalize globalenv env allow_patvar lvar c =
     (* the "in" part *)
     let match_td,typ = match t with
     | Some t ->
-	let with_letin,(ind,l) = intern_ind_pattern globalenv (None,env.scopes) t in
+	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 (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")])