10 files changed, 103 insertions, 2 deletions
diff --git a/test-suite/bugs/closed/bug_3468.v b/test-suite/bugs/closed/bug_3468.v
new file mode 100644
index 0000000000..6ff394bca6
--- /dev/null
+++ b/test-suite/bugs/closed/bug_3468.v
@@ -0,0 +1,29 @@
+(* Checking that unrelated terms requiring some scope do not affect
+   the interpretation of tactic-in-term. The "Check" was failing with:
+   The term "Set" has type "Type" while it is expected to have type
+   "nat". *)
+
+Notation bar2 a b := (let __ := ltac:(exact I) in (a + b)%type) (only parsing).
+Check bar2 (Set + Set) Set.
+
+(* Taking into account scopes in notations containing tactic-in-term *)
+
+Declare Scope foo_scope.
+Delimit Scope foo_scope with foo.
+Notation "x ~~" := (x) (at level 0, only parsing) : foo_scope.
+Notation bar x := (x%foo) (only parsing).
+Notation baz x := ltac:(exact x%foo) (only parsing).
+Check bar (O ~~).
+Check baz (O ~~). (* Was failing *)
+
+(* This was reported as bug #8706 *)
+
+Declare Scope my_scope.
+Notation "@ a" := a%nat (at level 100, only parsing) : my_scope.
+Delimit Scope my_scope with my.
+
+Notation "& b" := ltac:(exact (b)%my) (at level 100, only parsing): my_scope.
+Definition test := (& (@4))%my.
+
+(* Check inconsistent scopes *)
+Fail Notation bar3 a := (let __ := ltac:(exact a%nat) in a%bool) (only parsing).
diff --git a/test-suite/bugs/closed/bug_8755.v b/test-suite/bugs/closed/bug_8755.v
new file mode 100644
index 0000000000..cd5aee4fa0
--- /dev/null
+++ b/test-suite/bugs/closed/bug_8755.v
@@ -0,0 +1,6 @@
+
+Lemma f : Type.
+Fail let i := ident:(i) in
+let t := context i [Type] in
+idtac.
+Abort.
diff --git a/test-suite/bugs/closed/bug_8848.v b/test-suite/bugs/closed/bug_8848.v
new file mode 100644
index 0000000000..26563e6747
--- /dev/null
+++ b/test-suite/bugs/closed/bug_8848.v
@@ -0,0 +1,18 @@
+Require Import Program.
+Set Implicit Arguments.
+Unset Strict Implicit.
+
+Definition def (a : nat) := a = a.
+
+Structure record {a : nat} {D : def a} :=
+  inR { prop : Prop }.
+
+Program
+Canonical Structure ins (a : nat) (rec : @record a _) :=
+  @inR a _ (prop rec).
+Next Obligation.
+  exact eq_refl.
+Defined.
+Next Obligation.
+  exact eq_refl.
+Defined.
diff --git a/test-suite/coqchk/bug_8655.v b/test-suite/coqchk/bug_8655.v
new file mode 100644
index 0000000000..06d08b2082
--- /dev/null
+++ b/test-suite/coqchk/bug_8655.v
@@ -0,0 +1 @@
+Inductive IND2 (A:Type) (T:=fun _ : Type->Type => A) := CONS2 : IND2 A -> IND2 (T IND2).
diff --git a/test-suite/coqchk/bug_8876.v b/test-suite/coqchk/bug_8876.v
new file mode 100644
index 0000000000..2d20511a04
--- /dev/null
+++ b/test-suite/coqchk/bug_8876.v
@@ -0,0 +1,19 @@
+(* -*- coq-prog-args: ("-noinit"); -*- *)
+Require Import Coq.Init.Notations.
+
+Notation "x -> y" := (forall _ : x, y).
+
+Inductive eq {A:Type} (a:A) : A -> Prop := eq_refl : eq a a.
+
+Set Universe Polymorphism.
+Set Polymorphic Inductive Cumulativity.
+Set Printing Universes.
+
+(* Constructors for an inductive with indices *)
+Module WithIndex.
+  Inductive foo@{i} : (Prop -> Prop) -> Prop := mkfoo: foo (fun x => x).
+
+  Monomorphic Universes i j.
+  Monomorphic Constraint i < j.
+  Definition bar : eq mkfoo@{i} mkfoo@{j} := eq_refl _.
+End WithIndex.
diff --git a/test-suite/coqchk/bug_8881.v b/test-suite/coqchk/bug_8881.v
new file mode 100644
index 0000000000..dfc209b318
--- /dev/null
+++ b/test-suite/coqchk/bug_8881.v
@@ -0,0 +1,23 @@
+
+(* Check use of equivalence on inductive types (bug #1242) *)
+
+Module Type ASIG.
+  Inductive t : Set := a | b : t.
+  Definition f := fun x => match x with a => true | b => false end.
+End ASIG.
+
+Module Type BSIG.
+  Declare Module A : ASIG.
+  Definition f := fun x => match x with A.a => true | A.b => false end.
+End BSIG.
+
+Module C (A : ASIG) (B : BSIG with Module A:=A).
+
+  (* Check equivalence is considered in "case_info" *)
+  Lemma test : forall x, A.f x = B.f x.
+  Proof.
+    intro x. unfold B.f, A.f.
+    destruct x; reflexivity.
+  Qed.
+
+End C.
diff --git a/test-suite/misc/poly-capture-global-univs/.gitignore b/test-suite/misc/poly-capture-global-univs/.gitignore
index f5a6d22b8e..2a6a6bc68d 100644
--- a/test-suite/misc/poly-capture-global-univs/.gitignore
+++ b/test-suite/misc/poly-capture-global-univs/.gitignore
@@ -1 +1,2 @@
 /Makefile*
+/src/evil.ml
diff --git a/test-suite/output/Notations4.out b/test-suite/output/Notations4.out
index cef7d1a702..46784d1897 100644
--- a/test-suite/output/Notations4.out
+++ b/test-suite/output/Notations4.out
@@ -1,5 +1,7 @@
 [< 0 > + < 1 > * < 2 >]
      : nat
+[< b > + < b > * < 2 >]
+     : nat
 [<< # 0 >>]
      : option nat
 [1 {f 1}]
diff --git a/test-suite/output/Notations4.v b/test-suite/output/Notations4.v
index 9738ce5a5e..6bdbf1bed5 100644
--- a/test-suite/output/Notations4.v
+++ b/test-suite/output/Notations4.v
@@ -10,6 +10,10 @@ Notation "x * y" := (Nat.mul x y) (in custom myconstr at level 4).
 Notation "< x >" := x (in custom myconstr at level 3, x constr at level 10).
 Check [ < 0 > + < 1 > * < 2 >].
 
+Axiom a : nat.
+Notation b := a.
+Check [ < b > + < a > * < 2 >].
+
 Declare Custom Entry anotherconstr.
 
 Notation "[ x ]" := x (x custom myconstr at level 6).
diff --git a/test-suite/success/Inductive.v b/test-suite/success/Inductive.v
index f07c0191f1..c2130995fc 100644
--- a/test-suite/success/Inductive.v
+++ b/test-suite/success/Inductive.v
@@ -1,7 +1,5 @@
 (* Test des definitions inductives imbriquees *)
 
-Require Import List.
-
 Inductive X : Set :=
     cons1 : list X -> X.