13 files changed, 203 insertions, 53 deletions

diff --git a/test-suite/success/CanonicalStructure.v b/test-suite/success/CanonicalStructure.v
index b8cae47196..88702a6e80 100644
--- a/test-suite/success/CanonicalStructure.v
+++ b/test-suite/success/CanonicalStructure.v
@@ -29,3 +29,44 @@ Canonical Structure bool_test := mk_test (fun x y => x || y).
 Definition b := bool.
 
 Check (fun x : b => x != x).
+
+Inductive four := x0 | x1 | x2 | x3.
+Structure local := MKL { l : four }.
+
+Section X.
+  Definition s0 := MKL x0.
+  #[local] Canonical Structure s0.
+  Check (refl_equal _ : l _ = x0).
+
+  #[local] Canonical Structure s1 := MKL x1.
+  Check (refl_equal _ : l _ = x1).
+
+  Local Canonical Structure s2 := MKL x2.
+  Check (refl_equal _ : l _ = x2).
+
+End X.
+Fail Check (refl_equal _ : l _ = x0).
+Fail Check (refl_equal _ : l _ = x1).
+Fail Check (refl_equal _ : l _ = x2).
+Check s0.
+Check s1.
+Check s2.
+
+Section Y.
+  Let s3 := MKL x3.
+  Canonical Structure s3.
+  Check (refl_equal _ : l _ = x3).
+End Y.
+Fail Check (refl_equal _ : l _ = x3).
+Fail Check s3.
+
+Section V.
+  #[canonical] Let s3 := MKL x3.
+  Check (refl_equal _ : l _ = x3).
+End V.
+
+Section W.
+  #[canonical, local] Definition s2' := MKL x2.
+  Check (refl_equal _ : l _ = x2).
+End W.
+Fail Check (refl_equal _ : l _ = x2).
diff --git a/test-suite/success/Inductive.v b/test-suite/success/Inductive.v
index c2130995fc..4b2d4457bf 100644
--- a/test-suite/success/Inductive.v
+++ b/test-suite/success/Inductive.v
@@ -71,7 +71,7 @@ CoInductive LList (A : Set) : Set :=
   | LNil : LList A
   | LCons : A -> LList A -> LList A.
 
-Arguments LNil [A].
+Arguments LNil {A}.
 
 Inductive Finite (A : Set) : LList A -> Prop :=
   | Finite_LNil : Finite LNil
@@ -204,3 +204,19 @@ End NonRecLetIn.
 
 Fail Inductive foo (T : Type) : let T := Type in T :=
   { r : forall x : T, x = x }.
+
+Module Discharge.
+  (* discharge test *)
+  Section S.
+    Let x := Prop.
+    Inductive foo : x := bla : foo.
+  End S.
+  Check bla:foo.
+
+  Section S.
+    Variables (A:Type).
+    (* ensure params are scanned for needed section variables even with template arity *)
+    #[universes(template)] Inductive bar (d:A) := .
+  End S.
+  Check @bar nat 0.
+End Discharge.
diff --git a/test-suite/success/Inversion.v b/test-suite/success/Inversion.v
index 1dbeaf3e1f..8297f54641 100644
--- a/test-suite/success/Inversion.v
+++ b/test-suite/success/Inversion.v
@@ -31,7 +31,7 @@ Inductive in_extension (I : Set) (r : rule I) : extension I -> Type :=
   | in_first : forall e, in_extension r (add_rule r e)
   | in_rest : forall e r', in_extension r e -> in_extension r (add_rule r' e).
 
-Arguments NL [I].
+Arguments NL {I}.
 
 Inductive super_extension (I : Set) (e : extension I) :
 extension I -> Type :=
diff --git a/test-suite/success/NotationDeprecation.v b/test-suite/success/NotationDeprecation.v
index 96814a1b97..60d40d3d12 100644
--- a/test-suite/success/NotationDeprecation.v
+++ b/test-suite/success/NotationDeprecation.v
@@ -3,19 +3,11 @@ Module Syndefs.
 #[deprecated(since = "8.9", note = "Do not use.")]
 Notation foo := Prop.
 
-Notation bar := Prop (compat "8.9").
-
-Fail
-#[deprecated(since = "8.9", note = "Do not use.")]
-Notation zar := Prop (compat "8.9").
-
 Check foo.
-Check bar.
 
 Set Warnings "+deprecated".
 
 Fail Check foo.
-Fail Check bar.
 
 End Syndefs.
 
@@ -24,19 +16,11 @@ Module Notations.
 #[deprecated(since = "8.9", note = "Do not use.")]
 Notation "!!" := Prop.
 
-Notation "##" := Prop (compat "8.9").
-
-Fail
-#[deprecated(since = "8.9", note = "Do not use.")]
-Notation "**" := Prop (compat "8.9").
-
 Check !!.
-Check ##.
 
 Set Warnings "+deprecated".
 
 Fail Check !!.
-Fail Check ##.
 
 End Notations.
 
@@ -45,18 +29,10 @@ Module Infix.
 #[deprecated(since = "8.9", note = "Do not use.")]
 Infix "!!" := plus (at level 1).
 
-Infix "##" := plus (at level 1, compat "8.9").
-
-Fail
-#[deprecated(since = "8.9", note = "Do not use.")]
-Infix "**" := plus (at level 1, compat "8.9").
-
 Check (_ !! _).
-Check (_ ## _).
 
 Set Warnings "+deprecated".
 
 Fail Check (_ !! _).
-Fail Check (_ ## _).
 
 End Infix.
diff --git a/test-suite/success/Notations2.v b/test-suite/success/Notations2.v
index d047f7560e..aa439fae12 100644
--- a/test-suite/success/Notations2.v
+++ b/test-suite/success/Notations2.v
@@ -165,3 +165,10 @@ Notation "# x ## t & u" := ((fun x => (x,t)),(fun x => (x,u))) (at level 0, x pa
 Check fun y : nat => # (x,z) ## y & y.
 
 End M17.
+
+Module Bug10750.
+
+Notation "#" := 0 (only printing).
+Print Visibility.
+
+End Bug10750.
diff --git a/test-suite/success/Omega.v b/test-suite/success/Omega.v
index 470e4f0580..5e0f90d59b 100644
--- a/test-suite/success/Omega.v
+++ b/test-suite/success/Omega.v
@@ -90,5 +90,5 @@ Qed.
 (* Postponed... problem with goals of the form "(n*m=0)%nat -> (n*m=0)%Z" *)
 Lemma lem10 : forall n m:nat, le n (plus n (mult n m)).
 Proof.
-intros; omega with *.
+intros; zify; omega.
 Qed.
diff --git a/test-suite/success/OmegaPre.v b/test-suite/success/OmegaPre.v
index 17531064cc..0223255067 100644
--- a/test-suite/success/OmegaPre.v
+++ b/test-suite/success/OmegaPre.v
@@ -16,112 +16,112 @@ Open Scope Z_scope.
 
 Goal forall a:Z, Z.max a a = a.
 intros.
-omega with *.
+zify; omega.
 Qed.
 
 Goal forall a b:Z, Z.max a b = Z.max b a.
 intros.
-omega with *.
+zify; omega.
 Qed.
 
 Goal forall a b c:Z, Z.max a (Z.max b c) = Z.max (Z.max a b) c.
 intros.
-omega with *.
+zify; omega.
 Qed.
 
 Goal forall a b:Z, Z.max a b + Z.min a b = a + b.
 intros.
-omega with *.
+zify; omega.
 Qed.
 
 Goal forall a:Z, (Z.abs a)*(Z.sgn a) = a.
 intros.
 zify.
-intuition; subst; omega. (* pure multiplication: omega alone can't do it *)
+intuition; subst; zify; omega. (* pure multiplication: zify; omega alone can't do it *)
 Qed.
 
 Goal forall a:Z, Z.abs a = a -> a >= 0.
 intros.
-omega with *.
+zify; omega.
 Qed.
 
 Goal forall a:Z, Z.sgn a = a -> a = 1 \/ a = 0 \/ a = -1.
 intros.
-omega with *.
+zify; omega.
 Qed.
 
 (* zify_nat *)
 
 Goal forall m: nat, (m<2)%nat -> (0<= m+m <=2)%nat.
 intros.
-omega with *.
+zify; omega.
 Qed.
 
 Goal forall m:nat, (m<1)%nat -> (m=0)%nat.
 intros.
-omega with *.
+zify; omega.
 Qed.
 
 Goal forall m: nat, (m<=100)%nat -> (0<= m+m <=200)%nat.
 intros.
-omega with *.
+zify; omega.
 Qed.
 (* 2000 instead of 200: works, but quite slow *)
 
 Goal forall m: nat, (m*m>=0)%nat.
 intros.
-omega with *.
+zify; omega.
 Qed.
 
 (* zify_positive *)
 
 Goal forall m: positive, (m<2)%positive -> (2 <= m+m /\ m+m <= 2)%positive.
 intros.
-omega with *.
+zify; omega.
 Qed.
 
 Goal forall m:positive, (m<2)%positive -> (m=1)%positive.
 intros.
-omega with *.
+zify; omega.
 Qed.
 
 Goal forall m: positive, (m<=1000)%positive -> (2<=m+m/\m+m <=2000)%positive.
 intros.
-omega with *.
+zify; omega.
 Qed.
 
 Goal forall m: positive, (m*m>=1)%positive.
 intros.
-omega with *.
+zify; omega.
 Qed.
 
 (* zify_N *)
 
 Goal forall m:N, (m<2)%N -> (0 <= m+m /\ m+m <= 2)%N.
 intros.
-omega with *.
+zify; omega.
 Qed.
 
 Goal forall m:N, (m<1)%N -> (m=0)%N.
 intros.
-omega with *.
+zify; omega.
 Qed.
 
 Goal forall m:N, (m<=1000)%N -> (0<=m+m/\m+m <=2000)%N.
 intros.
-omega with *.
+zify; omega.
 Qed.
 
 Goal forall m:N, (m*m>=0)%N.
 intros.
-omega with *.
+zify; omega.
 Qed.
 
 (* mix of datatypes *)
 
 Goal forall p, Z.of_N (N.of_nat (N.to_nat (Npos p))) = Zpos p.
 intros.
-omega with *.
+zify; omega.
 Qed.
 
 
diff --git a/test-suite/success/RecTutorial.v b/test-suite/success/RecTutorial.v
index 6370cab6b2..15672eab7c 100644
--- a/test-suite/success/RecTutorial.v
+++ b/test-suite/success/RecTutorial.v
@@ -994,7 +994,7 @@ Qed.
 
 
 Arguments Vector.cons [A] _ [n].
-Arguments Vector.nil [A].
+Arguments Vector.nil {A}.
 Arguments Vector.hd [A n].
 Arguments Vector.tl [A n].
 
@@ -1161,7 +1161,7 @@ infiniteproof map_iterate'.
 Qed.
 
 
-Arguments LNil [A].
+Arguments LNil {A}.
 
 Lemma Lnil_not_Lcons : forall (A:Set)(a:A)(l:LList A),
                                LNil <> (LCons a l).
@@ -1210,7 +1210,3 @@ Proof.
  constructor.
  trivial.
 Qed.
-
-
-
-
diff --git a/test-suite/success/cofixtac.v b/test-suite/success/cofixtac.v
new file mode 100644
index 0000000000..ae75ee770f
--- /dev/null
+++ b/test-suite/success/cofixtac.v
@@ -0,0 +1,10 @@
+CoInductive stream :=
+| C : content -> stream
+with content :=
+| D : nat -> stream -> content.
+
+Lemma one : stream.
+cofix c with (d : content).
+- constructor. apply d.
+- constructor. exact 1. apply c.
+Defined.
diff --git a/test-suite/success/custom_entry.v b/test-suite/success/custom_entry.v
new file mode 100644
index 0000000000..e88ae65e18
--- /dev/null
+++ b/test-suite/success/custom_entry.v
@@ -0,0 +1,13 @@
+Declare Custom Entry foo.
+
+Print Custom Grammar foo.
+
+Notation "[ e ]" := e (e custom foo at level 0).
+
+Print Custom Grammar foo.
+
+Notation "1" := O (in custom foo at level 0).
+
+Print Custom Grammar foo.
+
+Fail Declare Custom Entry foo.
diff --git a/test-suite/success/implicit.v b/test-suite/success/implicit.v
index 23853890d8..ecaaedca53 100644
--- a/test-suite/success/implicit.v
+++ b/test-suite/success/implicit.v
@@ -124,3 +124,36 @@ Inductive I3 {A} (x:=0) (a:A) : forall {n:nat}, Prop :=
 (* Check global implicit declaration over ref not in section *)
 
 Section D. Global Arguments eq [A] _ _. End D.
+
+(* Check local manual implicit arguments *)
+(* Gives a warning and make the second x anonymous *)
+(* Isn't the name "arg_1" a bit fragile though? *)
+
+Check fun f : forall {x:nat} {x:bool} (x:unit), unit => f (x:=1) (arg_2:=true) tt.
+
+(* Check the existence of a shadowing warning *)
+
+Set Warnings "+syntax".
+Fail Check fun f : forall {x:nat} {x:bool} (x:unit), unit => f (x:=1) (arg_2:=true) tt.
+Set Warnings "syntax".
+
+(* Test failure when implicit arguments are mentioned in subterms
+   which are not types of variables *)
+
+Set Warnings "+syntax".
+Fail Check (id (forall {a}, a)).
+Set Warnings "syntax".
+
+(* Miscellaneous tests *)
+
+Check let f := fun {x:nat} y => y=true in f false.
+
+(* Isn't the name "arg_1" a bit fragile, here? *)
+
+Check fun f : forall {_:nat}, nat => f (arg_1:=0).
+
+(* This test was wrongly warning/failing at some time *)
+
+Set Warnings "+syntax".
+Check id (fun x => let f c {a} (b:a=a) := b in f true (eq_refl 0)).
+Set Warnings "syntax".
diff --git a/test-suite/success/rapply.v b/test-suite/success/rapply.v
new file mode 100644
index 0000000000..13efd986f0
--- /dev/null
+++ b/test-suite/success/rapply.v
@@ -0,0 +1,27 @@
+Require Import Coq.Program.Tactics.
+
+(** We make a version of [rapply] that takes [uconstr]; we do not
+currently test what scope [rapply] interprets terms in. *)
+
+Tactic Notation "urapply" uconstr(p) := rapply p.
+
+Ltac test n :=
+  (*let __ := match goal with _ => idtac n end in*)
+  lazymatch n with
+  | O => let __ := match goal with _ => assert True by urapply I; clear end in
+         uconstr:(fun _ => I)
+  | S ?n'
+    => let lem := test n' in
+       let __ := match goal with _ => assert True by (unshelve urapply lem; try exact I); clear end in
+       uconstr:(fun _ : True => lem)
+  end.
+
+Goal True.
+  assert True by urapply I.
+  assert True by (unshelve urapply (fun _ => I); try exact I).
+  assert True by (unshelve urapply (fun _ _ => I); try exact I).
+  assert True by (unshelve urapply (fun _ _ _ => I); try exact I).
+  clear.
+  Time let __ := test 50 in idtac.
+  urapply I.
+Qed.
diff --git a/test-suite/success/specialize.v b/test-suite/success/specialize.v
index f12db8b081..1122b9fa34 100644
--- a/test-suite/success/specialize.v
+++ b/test-suite/success/specialize.v
@@ -109,6 +109,37 @@ match goal with H:_ |- _ => clear H end.
 match goal with H:_ |- _ => exact H end.
 Qed.
 
+
+(* let ins should be supported int he type of the specialized hypothesis *)
+Axiom foo: forall (m1:nat) (m2: nat), let n := 2 * m1 in (m1 = m2 -> False).
+Goal False.
+  pose proof foo as P.
+  assert (2 = 2) as A by reflexivity.
+  (* specialize P with (m2:= 2). *)
+  specialize P with (1 := A).
+  match type of P with
+  | let n := 2 * 2 in False => idtac
+  | _ => fail "test failed"
+  end.
+  assumption.
+Qed.
+
+(* Another more subtle test on letins: they should not interfere with foralls. *)
+Goal forall (P: forall a c:nat,
+                  let b := c in
+                  let d := 1 in
+                  forall n : a = d, a = c+1),
+    True.
+  intros P.
+  specialize P with (1:=eq_refl).
+  match type of P with
+  | forall c : nat, let f := c in let d := 1 in 1 = c + 1 => idtac
+  | _ => fail "test failed"
+  end.
+  constructor.
+Qed.
+
+
 (* Test specialize as *)
 
 Goal (forall x, x=0) -> 1=0.