Fixing #5277 (Scheme Equality not robust wrt choice of names).

This is only a quick fix, as hinted by Jason.

2 files changed, 29 insertions, 13 deletions

diff --git a/test-suite/bugs/closed/5277.v b/test-suite/bugs/closed/5277.v
new file mode 100644
index 000000000..7abc38bfc
--- /dev/null
+++ b/test-suite/bugs/closed/5277.v
@@ -0,0 +1,11 @@
+(* Scheme Equality not robust wrt names *)
+
+Module A1.
+  Inductive A (T : Type) := C (a : T).
+  Scheme Equality for A. (* success *)
+End A1.
+
+Module A2.
+  Inductive A (x : Type) := C (a : x).
+  Scheme Equality for A. 
+End A2.
diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml
index b1811d6a6..f4b0b1b77 100644
--- a/toplevel/auto_ind_decl.ml
+++ b/toplevel/auto_ind_decl.ml
@@ -520,12 +520,15 @@ let eqI ind l =
 (**********************************************************************)
 (* Boolean->Leibniz *)
 
+open Namegen
+
 let compute_bl_goal ind lnamesparrec nparrec =
   let eqI, eff = eqI ind lnamesparrec in
   let list_id = list_id lnamesparrec in
+  let avoid = List.fold_right (Nameops.name_fold (fun id l -> id::l)) (List.map RelDecl.get_name lnamesparrec) [] in
   let create_input c =
-    let x = Id.of_string "x" and
-        y = Id.of_string "y" in
+    let x = next_ident_away (Id.of_string "x") avoid and
+        y = next_ident_away (Id.of_string "y") avoid in
       let bl_typ = List.map (fun (s,seq,_,_) ->
         mkNamedProd x (mkVar s) (
             mkNamedProd y (mkVar s) (
@@ -544,11 +547,11 @@ let compute_bl_goal ind lnamesparrec nparrec =
         mkNamedProd seq b a
       ) bl_input (List.rev list_id) (List.rev eqs_typ) in
       List.fold_left (fun a decl -> mkNamedProd
-                (match RelDecl.get_name decl with Name s -> s | Anonymous ->  Id.of_string "A")
+                (match RelDecl.get_name decl with Name s -> s | Anonymous -> next_ident_away (Id.of_string "A") avoid)
                 (RelDecl.get_type decl) a) eq_input lnamesparrec
     in
-      let n = Id.of_string "x" and
-          m = Id.of_string "y" in
+      let n = next_ident_away (Id.of_string "x") avoid and
+          m = next_ident_away (Id.of_string "y") avoid in
       let u = Univ.Instance.empty in
      create_input (
         mkNamedProd n (mkFullInd (ind,u) nparrec) (
@@ -665,10 +668,11 @@ let _ = bl_scheme_kind_aux := fun () -> bl_scheme_kind
 let compute_lb_goal ind lnamesparrec nparrec =
   let list_id = list_id lnamesparrec in
   let eq = Lazy.force eq and tt = Lazy.force tt and bb = Lazy.force bb in
+  let avoid = List.fold_right (Nameops.name_fold (fun id l -> id::l)) (List.map RelDecl.get_name lnamesparrec) [] in
   let eqI, eff = eqI ind lnamesparrec in
     let create_input c =
-      let x = Id.of_string "x" and
-          y = Id.of_string "y" in
+      let x = next_ident_away (Id.of_string "x") avoid and
+          y = next_ident_away (Id.of_string "y") avoid in
       let lb_typ = List.map (fun (s,seq,_,_) ->
         mkNamedProd x (mkVar s) (
             mkNamedProd y (mkVar s) (
@@ -690,8 +694,8 @@ let compute_lb_goal ind lnamesparrec nparrec =
                 (match (RelDecl.get_name decl) with Name s -> s | Anonymous ->  Id.of_string "A")
                 (RelDecl.get_type decl)  a) eq_input lnamesparrec
     in
-      let n = Id.of_string "x" and
-          m = Id.of_string "y" in
+      let n = next_ident_away (Id.of_string "x") avoid and
+          m = next_ident_away (Id.of_string "y") avoid in
       let u = Univ.Instance.empty in
       create_input (
         mkNamedProd n (mkFullInd (ind,u) nparrec) (
@@ -794,9 +798,10 @@ let compute_dec_goal ind lnamesparrec nparrec =
   check_not_is_defined ();
   let eq = Lazy.force eq and tt = Lazy.force tt and bb = Lazy.force bb in
   let list_id = list_id lnamesparrec in
+  let avoid = List.fold_right (Nameops.name_fold (fun id l -> id::l)) (List.map RelDecl.get_name lnamesparrec) [] in
     let create_input c =
-      let x = Id.of_string "x" and
-          y = Id.of_string "y" in
+      let x = next_ident_away (Id.of_string "x") avoid and
+          y = next_ident_away (Id.of_string "y") avoid in
       let lb_typ = List.map (fun (s,seq,_,_) ->
         mkNamedProd x (mkVar s) (
             mkNamedProd y (mkVar s) (
@@ -831,8 +836,8 @@ let compute_dec_goal ind lnamesparrec nparrec =
                 (match RelDecl.get_name decl with Name s -> s | Anonymous ->  Id.of_string "A")
                 (RelDecl.get_type decl) a) eq_input lnamesparrec
     in
-      let n = Id.of_string "x" and
-          m = Id.of_string "y" in
+      let n = next_ident_away (Id.of_string "x") avoid and
+          m = next_ident_away (Id.of_string "y") avoid in
         let eqnm = mkApp(eq,[|mkFullInd ind (2*nparrec+2);mkVar n;mkVar m|]) in
         create_input (
           mkNamedProd n (mkFullInd ind (2*nparrec)) (