15 files changed, 265 insertions, 4 deletions
diff --git a/test-suite/bugs/closed/bug_12348.v b/test-suite/bugs/closed/bug_12348.v
new file mode 100644
index 0000000000..93ba6f17e0
--- /dev/null
+++ b/test-suite/bugs/closed/bug_12348.v
@@ -0,0 +1,11 @@
+(* Was raising an anomaly before 8.13 *)
+Check let 'tt := tt in
+      let X := nat in
+      let b : bool := _ in
+      (fun n : nat => 0 : X) : _.
+
+(* Was raising an ill-typed instance error before 8.13 *)
+Check let 'tt := tt in
+      let X := nat in
+      let b : bool := true in
+      (fun n : nat => 0 : X) : _.
diff --git a/test-suite/bugs/closed/bug_13363.v b/test-suite/bugs/closed/bug_13363.v
new file mode 100644
index 0000000000..cc11aa93b6
--- /dev/null
+++ b/test-suite/bugs/closed/bug_13363.v
@@ -0,0 +1,17 @@
+Axiom X : Type.       
+Axiom P : (X -> unit) -> Prop.
+
+Axiom F: unit -> unit.
+Axiom G : unit -> unit.
+
+Lemma Hyp ss':
+    P (fun y : X => ss') ->
+    P (fun y : X => G (F ss')).
+Admitted.
+
+Lemma bug : exists x, P x.
+Proof.
+intros.
+eexists (fun y : X => G _).
+eapply Hyp. cbn beta.
+Abort.
diff --git a/test-suite/bugs/closed/bug_3513.v b/test-suite/bugs/closed/bug_3513.v
index 462a615d91..f3a19c2b89 100644
--- a/test-suite/bugs/closed/bug_3513.v
+++ b/test-suite/bugs/closed/bug_3513.v
@@ -13,7 +13,7 @@ Infix "|--"  := lentails (at level 79, no associativity).
 Class ILogic Frm {ILOps: ILogicOps Frm} := { lentailsPre:> PreOrder lentails }.
 Definition lequiv `{ILogic Frm} P Q := P |-- Q /\ Q |-- P.
 Infix "-|-"  := lequiv (at level 85, no associativity).
-Instance lequiv_inverse_lentails `{ILogic Frm} : subrelation lequiv (inverse lentails) := admit.
+Instance lequiv_inverse_lentails `{ILogic Frm} {inverse} : subrelation lequiv (inverse lentails) := admit.
 Record ILFunFrm (T : Type) `{e : Equiv T} `{ILOps : ILogicOps Frm} := mkILFunFrm { ILFunFrm_pred :> T -> Frm }.
 Section ILogic_Fun.
   Context (T: Type) `{TType: type T}.
diff --git a/test-suite/bugs/closed/bug_4095.v b/test-suite/bugs/closed/bug_4095.v
index d667022e68..2d4d7d02cc 100644
--- a/test-suite/bugs/closed/bug_4095.v
+++ b/test-suite/bugs/closed/bug_4095.v
@@ -15,7 +15,7 @@ Infix "|--"  := lentails (at level 79, no associativity).
 Class ILogic Frm {ILOps: ILogicOps Frm} := { lentailsPre:> PreOrder lentails }.
 Definition lequiv `{ILogic Frm} P Q := P |-- Q /\ Q |-- P.
 Infix "-|-"  := lequiv (at level 85, no associativity).
-Instance lequiv_inverse_lentails `{ILogic Frm} : subrelation lequiv (inverse lentails) := admit.
+Instance lequiv_inverse_lentails `{ILogic Frm} {inverse} : subrelation lequiv (inverse lentails) := admit.
 Record ILFunFrm (T : Type) `{e : Equiv T} `{ILOps : ILogicOps Frm} := mkILFunFrm { ILFunFrm_pred :> T -> Frm }.
 Section ILogic_Fun.
   Context (T: Type) `{TType: type T}.
diff --git a/test-suite/bugs/closed/bug_5512.v b/test-suite/bugs/closed/bug_5512.v
new file mode 100644
index 0000000000..f885e31352
--- /dev/null
+++ b/test-suite/bugs/closed/bug_5512.v
@@ -0,0 +1,10 @@
+(* Check that an anomaly is not raised *)
+(* It should however eventually succeed... *)
+Goal exists x, x.
+Proof.
+simple refine (ex_intro _ _ _).
+shelve.
+(* The failure is due to Type(u)<=Prop for u an arbitrary sort
+   variable being rejected *)
+Fail simple refine (_ _).
+Abort.
diff --git a/test-suite/bugs/closed/bug_6042.v b/test-suite/bugs/closed/bug_6042.v
new file mode 100644
index 0000000000..72f612560b
--- /dev/null
+++ b/test-suite/bugs/closed/bug_6042.v
@@ -0,0 +1,7 @@
+Class C (n: nat) := T{x:True}.
+Generalizable All Variables.
+
+Fail Instance i : C n.
+
+Instance i : `(C n).
+Proof. repeat constructor. Defined.
diff --git a/test-suite/output/HintLocality.out b/test-suite/output/HintLocality.out
new file mode 100644
index 0000000000..37a0613b25
--- /dev/null
+++ b/test-suite/output/HintLocality.out
@@ -0,0 +1,92 @@
+Non-discriminated database
+Unfoldable variable definitions: all
+Unfoldable constant definitions: all except: id
+Cut: _
+For any goal ->   
+For nat ->   
+For S (modes !) ->   
+
+Non-discriminated database
+Unfoldable variable definitions: all
+Unfoldable constant definitions: all except: id
+Cut: _
+For any goal ->   
+For nat ->   
+For S (modes !) ->   
+
+Non-discriminated database
+Unfoldable variable definitions: all
+Unfoldable constant definitions: all except: id
+Cut: _
+For any goal ->   
+For nat ->   
+For S (modes !) ->   
+
+Non-discriminated database
+Unfoldable variable definitions: all
+Unfoldable constant definitions: all except: id
+Cut: _
+For any goal ->   
+For nat ->   
+For S (modes !) ->   
+
+Non-discriminated database
+Unfoldable variable definitions: all
+Unfoldable constant definitions: all
+Cut: emp
+For any goal ->   
+For nat ->   simple apply 0 ; trivial(level 1, pattern nat, id 0) 
+
+Non-discriminated database
+Unfoldable variable definitions: all
+Unfoldable constant definitions: all
+Cut: emp
+For any goal ->   
+For nat ->   simple apply 0 ; trivial(level 1, pattern nat, id 0) 
+
+Non-discriminated database
+Unfoldable variable definitions: all
+Unfoldable constant definitions: all except: id
+Cut: _
+For any goal ->   
+For nat ->   
+For S (modes !) ->   
+
+Non-discriminated database
+Unfoldable variable definitions: all
+Unfoldable constant definitions: all
+Cut: emp
+For any goal ->   
+For nat ->   simple apply 0 ; trivial(level 1, pattern nat, id 0) 
+
+Non-discriminated database
+Unfoldable variable definitions: all
+Unfoldable constant definitions: all except: id
+Cut: _
+For any goal ->   
+For nat ->   
+For S (modes !) ->   
+
+The command has indeed failed with message:
+This command does not support the global attribute in sections.
+The command has indeed failed with message:
+This command does not support the global attribute in sections.
+The command has indeed failed with message:
+This command does not support the global attribute in sections.
+The command has indeed failed with message:
+This command does not support the global attribute in sections.
+Non-discriminated database
+Unfoldable variable definitions: all
+Unfoldable constant definitions: all except: id
+Cut: _
+For any goal ->   
+For nat ->   
+For S (modes !) ->   
+
+Non-discriminated database
+Unfoldable variable definitions: all
+Unfoldable constant definitions: all
+Cut: emp
+For any goal ->   
+For nat ->   simple apply 0 ; trivial(level 1, pattern nat, id 0) 
+
diff --git a/test-suite/output/HintLocality.v b/test-suite/output/HintLocality.v
new file mode 100644
index 0000000000..4481335907
--- /dev/null
+++ b/test-suite/output/HintLocality.v
@@ -0,0 +1,72 @@
+(** Test hint command locality w.r.t. modules *)
+
+Create HintDb foodb.
+Create HintDb bardb.
+Create HintDb quxdb.
+
+#[global] Hint Immediate O : foodb.
+#[global] Hint Immediate O : bardb.
+#[global] Hint Immediate O : quxdb.
+
+Module Test.
+
+#[global] Hint Cut [ _ ] : foodb.
+#[global] Hint Mode S ! : foodb.
+#[global] Hint Opaque id : foodb.
+#[global] Remove Hints O : foodb.
+
+#[local] Hint Cut [ _ ] : bardb.
+#[local] Hint Mode S ! : bardb.
+#[local] Hint Opaque id : bardb.
+#[local] Remove Hints O : bardb.
+
+#[export] Hint Cut [ _ ] : quxdb.
+#[export] Hint Mode S ! : quxdb.
+#[export] Hint Opaque id : quxdb.
+#[export] Remove Hints O : quxdb.
+
+(** All three agree here *)
+
+Print HintDb foodb.
+Print HintDb bardb.
+Print HintDb quxdb.
+
+End Test.
+
+(** bardb and quxdb agree here *)
+
+Print HintDb foodb.
+Print HintDb bardb.
+Print HintDb quxdb.
+
+Import Test.
+
+(** foodb and quxdb agree here *)
+
+Print HintDb foodb.
+Print HintDb bardb.
+Print HintDb quxdb.
+
+(** Test hint command locality w.r.t. sections *)
+
+Create HintDb secdb.
+
+#[global] Hint Immediate O : secdb.
+
+Section Sec.
+
+Fail #[global] Hint Cut [ _ ] : secdb.
+Fail #[global] Hint Mode S ! : secdb.
+Fail #[global] Hint Opaque id : secdb.
+Fail #[global] Remove Hints O : secdb.
+
+#[local] Hint Cut [ _ ] : secdb.
+#[local] Hint Mode S ! : secdb.
+#[local] Hint Opaque id : secdb.
+#[local] Remove Hints O : secdb.
+
+Print HintDb secdb.
+
+End Sec.
+
+Print HintDb secdb.
diff --git a/test-suite/output/Tactics.out b/test-suite/output/Tactics.out
index 70427220ed..3f07261ca6 100644
--- a/test-suite/output/Tactics.out
+++ b/test-suite/output/Tactics.out
@@ -7,3 +7,5 @@ H is already used.
 The command has indeed failed with message:
 H is already used.
 a
+The command has indeed failed with message:
+This variable is used in hypothesis H.
diff --git a/test-suite/output/Tactics.v b/test-suite/output/Tactics.v
index 96b6d652c9..8526e43a23 100644
--- a/test-suite/output/Tactics.v
+++ b/test-suite/output/Tactics.v
@@ -30,3 +30,11 @@ Goal True.
   assert_succeeds should_not_loop.
   assert_succeeds (idtac "a" + idtac "b"). (* should only output "a" *)
 Abort.
+
+Module IntroWildcard.
+
+Theorem foo : { p:nat*nat & p = (0,0) } -> True.
+Fail intros ((n,_),H).
+Abort.
+
+End IntroWildcard.
diff --git a/test-suite/output/TypeclassDebug.v b/test-suite/output/TypeclassDebug.v
index 2e4008ae56..0bd3d5fa40 100644
--- a/test-suite/output/TypeclassDebug.v
+++ b/test-suite/output/TypeclassDebug.v
@@ -2,6 +2,7 @@
 
 Parameter foo : Prop.
 Axiom H : foo -> foo.
+#[global]
 Hint Resolve H : foo.
 Goal foo.
 Typeclasses eauto := debug.
diff --git a/test-suite/output/locate.out b/test-suite/output/locate.out
index 93d9d6cf7b..0196ead5e4 100644
--- a/test-suite/output/locate.out
+++ b/test-suite/output/locate.out
@@ -1,2 +1,8 @@
 Notation "b1 && b2" := (if b1 then b2 else false) (default interpretation)
 Notation "x && y" := (andb x y) : bool_scope
+Notation "'U' t" := (S t) (default interpretation)
+Notation "'_' t" := (S t) (default interpretation)
+Notation "( x , y , .. , z )" := (pair .. (pair x y) .. z) : core_scope (default interpretation)
+Notation "( x , y , .. , z )" := (pair .. (pair x y) .. z) : core_scope (default interpretation)
+Notation "( x , y , .. , z )" := (pair .. (pair x y) .. z) : core_scope (default interpretation)
+Notation "( x , y , .. , z )" := (pair .. (pair x y) .. z) : core_scope (default interpretation)
diff --git a/test-suite/output/locate.v b/test-suite/output/locate.v
index af8b0ee193..6995743531 100644
--- a/test-suite/output/locate.v
+++ b/test-suite/output/locate.v
@@ -1,3 +1,26 @@
 Set Printing Width 400.
 Notation "b1 && b2" := (if b1 then b2 else false).
 Locate "&&".
+
+Module M.
+
+Notation "'U' t" := (S t) (at level 0).
+Notation "'_' t" := (S t) (at level 0).
+Locate "U". (* was wrongly returning also "'_' t" *)
+Locate "_".
+
+End M.
+
+Module N.
+
+(* Was not working at some time *)
+Locate "( t , u , .. , v )".
+
+(* Was working though *)
+Locate "( _ , _ , .. , _ )".
+
+(* We also support this *)
+Locate "( t , u )".
+Locate "( t , u , v )".
+
+End N.
diff --git a/test-suite/success/Notations2.v b/test-suite/success/Notations2.v
index 382c252727..fb8bbfd043 100644
--- a/test-suite/success/Notations2.v
+++ b/test-suite/success/Notations2.v
@@ -51,8 +51,8 @@ Check fun A (x : prod' bool A) => match x with (@pair' _ 0) _ y 0%bool => 2 | _
 Notation c3 x := ((@pair') _ x).
 Check (@pair') _ 0%bool _ 0%bool 0%bool : prod' bool bool. (* @ is blocking implicit and scopes *)
 Check ((@pair') _ 0%bool) _ 0%bool 0%bool : prod' bool bool. (* parentheses and @ are blocking implicit and scopes *)
-Check c3 0 0 0 : prod' nat bool. (* First scope is blocked but not the last two scopes *)
-Check fun A (x :prod' nat A) => match x with c3 0 y 0 => 2 | _ => 1 end.
+Check c3 0 0 0 : prod' bool bool.
+Check fun A (x :prod' bool A) => match x with c3 0 y 0 => 2 | _ => 1 end.
 
 (* 4. Abbreviations do not stop implicit arguments to be inserted and scopes to be used *)
 (* unless an atomic @ is given *)
diff --git a/test-suite/success/Scopes.v b/test-suite/success/Scopes.v
index 06697af901..8b7d239dcd 100644
--- a/test-suite/success/Scopes.v
+++ b/test-suite/success/Scopes.v
@@ -26,3 +26,15 @@ Definition c := ε : U.
 Goal True.
 assert (nat * nat).
 Abort.
+
+(* Check propagation of scopes in indirect applications to references *)
+
+Module PropagateIndirect.
+Notation "0" := true : bool_scope.
+
+Axiom f : bool -> bool -> nat.
+Check (@f 0) 0.
+
+Record R := { p : bool -> nat }.
+Check fun r => r.(@p) 0.
+End PropagateIndirect.