8 files changed, 39 insertions, 3 deletions
diff --git a/test-suite/bugs/closed/2417.v b/test-suite/bugs/closed/2417.v
new file mode 100644
index 000000000..b2f00ffc6
--- /dev/null
+++ b/test-suite/bugs/closed/2417.v
@@ -0,0 +1,15 @@
+Parameter x y : nat.
+Axiom H : x = y.
+Hint Rewrite H : mybase.
+
+Ltac bar base := autorewrite with base.
+
+Tactic Notation "foo" ident(base) := autorewrite with base.
+
+Goal x = 0.
+  bar mybase.
+  now_show (y = 0).
+  Undo 2.
+  foo mybase.
+  now_show (y = 0).
+Abort.
diff --git a/test-suite/bugs/closed/3612.v b/test-suite/bugs/closed/3612.v
index a54768507..4b4f81dbc 100644
--- a/test-suite/bugs/closed/3612.v
+++ b/test-suite/bugs/closed/3612.v
@@ -38,8 +38,11 @@ Axiom path_path_sigma : forall {A : Type} (P : A -> Type) (u v : sigT P)
            (s : transport (fun x => transport P x u.2 = v.2) r p..2 = q..2),
 p = q.
 
+Declare ML Module "ltac_plugin".
 Declare ML Module "coretactics".
 
+Set Default Proof Mode "Classic".
+
 Goal forall (A : Type) (B : forall _ : A, Type) (x : @sigT A (fun x : A => B x))
             (xx : @paths (@sigT A (fun x0 : A => B x0)) x x),
        @paths (@paths (@sigT A (fun x0 : A => B x0)) x x) xx
diff --git a/test-suite/bugs/closed/3649.v b/test-suite/bugs/closed/3649.v
index fc4c171e2..8687eaab0 100644
--- a/test-suite/bugs/closed/3649.v
+++ b/test-suite/bugs/closed/3649.v
@@ -2,7 +2,9 @@
 (* File reduced by coq-bug-finder from original input, then from 9518 lines to 404 lines, then from 410 lines to 208 lines, then from 162 lines to 77 lines *)
 (* coqc version trunk (September 2014) compiled on Sep 18 2014 21:0:5 with OCaml 4.01.0
    coqtop version cagnode16:/afs/csail.mit.edu/u/j/jgross/coq-trunk,trunk (07e4438bd758c2ced8caf09a6961ccd77d84e42b) *)
+Declare ML Module "ltac_plugin".
 Declare ML Module "coretactics".
+Set Default Proof Mode "Classic".
 Reserved Notation "x -> y" (at level 99, right associativity, y at level 200).
 Reserved Notation "x = y" (at level 70, no associativity).
 Delimit Scope type_scope with type.
diff --git a/test-suite/bugs/closed/4121.v b/test-suite/bugs/closed/4121.v
index d34a2b8b1..816bc845f 100644
--- a/test-suite/bugs/closed/4121.v
+++ b/test-suite/bugs/closed/4121.v
@@ -4,6 +4,8 @@ Unset Strict Universe Declaration.
 (* coqc version 8.5beta1 (March 2015) compiled on Mar 11 2015 18:51:36 with OCaml 4.01.0
    coqtop version cagnode15:/afs/csail.mit.edu/u/j/jgross/coq-8.5,v8.5 (8dbfee5c5f897af8186cb1bdfb04fd4f88eca677) *)
 
+Declare ML Module "ltac_plugin".
+
 Set Universe Polymorphism.
 Class Contr_internal (A : Type) := BuildContr { center : A }.
 Arguments center A {_}.
@@ -13,4 +15,4 @@ Definition contr_paths_contr0 {A} `{Contr A} : Contr A := {| center := center A
 Instance contr_paths_contr1 {A} `{Contr A} : Contr A := {| center := center A |}.
 Check @contr_paths_contr0@{i}.
 Check @contr_paths_contr1@{i}. (* Error: Universe instance should have length 2 *)
-(** It should have length 1, just like contr_paths_contr0 *)
-\ No newline at end of file
+(** It should have length 1, just like contr_paths_contr0 *)
diff --git a/test-suite/bugs/closed/4527.v b/test-suite/bugs/closed/4527.v
index 08628377f..c6fcc24b6 100644
--- a/test-suite/bugs/closed/4527.v
+++ b/test-suite/bugs/closed/4527.v
@@ -5,6 +5,7 @@ then from 269 lines to 255 lines *)
 (* coqc version 8.5 (January 2016) compiled on Jan 23 2016 16:15:22 with OCaml 
 4.01.0
    coqtop version 8.5 (January 2016) *)
+Declare ML Module "ltac_plugin".
 Inductive False := .
 Axiom proof_admitted : False.
 Tactic Notation "admit" := case proof_admitted.
diff --git a/test-suite/bugs/closed/4533.v b/test-suite/bugs/closed/4533.v
index ae17fb145..64c7fd8eb 100644
--- a/test-suite/bugs/closed/4533.v
+++ b/test-suite/bugs/closed/4533.v
@@ -5,6 +5,7 @@ then from 285 lines to 271 lines *)
 (* coqc version 8.5 (January 2016) compiled on Jan 23 2016 16:15:22 with OCaml 
 4.01.0
    coqtop version 8.5 (January 2016) *)
+Declare ML Module "ltac_plugin".
 Inductive False := .
 Axiom proof_admitted : False.
 Tactic Notation "admit" := case proof_admitted.
@@ -223,4 +224,4 @@ v = _) r,
     | [ |- p2 @ p0 @ p1 @ eissect (to O A) (g x) = r ] => idtac "good"
     | [ |- ?G ] => fail 1 "bad" G
     end.
-    Fail rewrite concat_p_pp.
-\ No newline at end of file
+    Fail rewrite concat_p_pp.
diff --git a/test-suite/bugs/closed/4544.v b/test-suite/bugs/closed/4544.v
index da140c931..64dd8c304 100644
--- a/test-suite/bugs/closed/4544.v
+++ b/test-suite/bugs/closed/4544.v
@@ -2,6 +2,7 @@
 (* File reduced by coq-bug-finder from original input, then from 2553 lines to 1932 lines, then from 1946 lines to 1932 lines, then from 2467 lines to 1002 lines, then from 1016 lines to 1002 lines *)
 (* coqc version 8.5 (January 2016) compiled on Jan 23 2016 16:15:22 with OCaml 4.01.0
    coqtop version 8.5 (January 2016) *)
+Declare ML Module "ltac_plugin".
 Inductive False := .
 Axiom proof_admitted : False.
 Tactic Notation "admit" := case proof_admitted.
@@ -1004,4 +1005,4 @@ Proof.
   Fail Timeout 1 Time rewrite !loops_functor_group.
   (* 0.004 s in 8.5rc1, 8.677 s in 8.5 *)
   Timeout 1 do 3 rewrite loops_functor_group.
-Abort.
-\ No newline at end of file
+Abort.
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.