12 files changed, 123 insertions, 62 deletions

diff --git a/test-suite/success/CanonicalStructure.v b/test-suite/success/CanonicalStructure.v
index e6d674c1e6..88702a6e80 100644
--- a/test-suite/success/CanonicalStructure.v
+++ b/test-suite/success/CanonicalStructure.v
@@ -51,3 +51,22 @@ 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/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/QArithSyntax.v b/test-suite/success/QArithSyntax.v
deleted file mode 100644
index 2f2ee0134a..0000000000
--- a/test-suite/success/QArithSyntax.v
+++ /dev/null
@@ -1,9 +0,0 @@
-Require Import QArith.
-Open Scope Q_scope.
-Check (eq_refl : 1.02 = 102 # 100).
-Check (eq_refl : 1.02e1 = 102 # 10).
-Check (eq_refl : 1.02e+03 = 1020).
-Check (eq_refl : 1.02e+02 = 102 # 1).
-Check (eq_refl : 10.2e-1 = 1.02).
-Check (eq_refl : -0.0001 = -1 # 10000).
-Check (eq_refl : -0.50 = - 50 # 100).
diff --git a/test-suite/success/RealSyntax.v b/test-suite/success/RealSyntax.v
deleted file mode 100644
index 2765200991..0000000000
--- a/test-suite/success/RealSyntax.v
+++ /dev/null
@@ -1,19 +0,0 @@
-Require Import Reals.
-Open Scope R_scope.
-Check (eq_refl : 1.02 = IZR 102 / IZR (Z.pow_pos 10 2)).
-Check (eq_refl : 1.02e1 = IZR 102 / IZR (Z.pow_pos 10 1)).
-Check (eq_refl : 1.02e+03 = IZR 102 * IZR (Z.pow_pos 10 1)).
-Check (eq_refl : 1.02e+02 = IZR 102).
-Check (eq_refl : 10.2e-1 = 1.02).
-Check (eq_refl : -0.0001 = IZR (-1) / IZR (Z.pow_pos 10 4)).
-Check (eq_refl : -0.5 = IZR (-5) / IZR (Z.pow_pos 10 1)).
-
-Goal 254e3 = 2540 * 10 ^ 2.
-ring.
-Qed.
-
-Require Import Psatz.
-
-Goal 254e3 = 2540 * 10 ^ 2.
-lra.
-Qed.
diff --git a/test-suite/success/RecTutorial.v b/test-suite/success/RecTutorial.v
index 4fac798f76..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).
diff --git a/test-suite/success/Scheme.v b/test-suite/success/Scheme.v
index 855f26698c..4b928007cf 100644
--- a/test-suite/success/Scheme.v
+++ b/test-suite/success/Scheme.v
@@ -25,3 +25,8 @@ Check myeq_rew_fwd_r_dep.
 Set Rewriting Schemes.
 Inductive myeq_true : bool -> Prop := myrefl_true : myeq_true true.
 Unset Rewriting Schemes.
+
+(* check that the scheme doesn't minimize itself into something non general *)
+Polymorphic Inductive foo@{u v|u<=v} : Type@{u}:= .
+Lemma bla@{u v|u < v} : foo@{u v} -> False.
+Proof. induction 1. Qed.
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/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 1b04594290..1122b9fa34 100644
--- a/test-suite/success/specialize.v
+++ b/test-suite/success/specialize.v
@@ -109,28 +109,37 @@ match goal with H:_ |- _ => clear H end.
 match goal with H:_ |- _ => exact H end.
 Qed.
 
-(* let ins should be supported in the type of the specialized hypothesis *)
-Axiom foo: forall (m1 m2: nat), let n := 2 * m1 in m1 = m2 -> False.
+
+(* 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 y:nat,
-                forall A (zz:A),
-                  let a := zz in
-                  let x := 1 in
-                  forall n : y = x,
-                    n = n),
+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 (zz := @eq_refl _ 2).
+  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.