8 files changed, 85 insertions, 7 deletions
diff --git a/test-suite/success/Abstract.v b/test-suite/success/Abstract.v
index ffd50f6efd..69dc9aca78 100644
--- a/test-suite/success/Abstract.v
+++ b/test-suite/success/Abstract.v
@@ -1,4 +1,3 @@
-
 (* Cf coqbugs #546 *)
 
 Require Import Omega.
diff --git a/test-suite/success/ImplicitArguments.v b/test-suite/success/ImplicitArguments.v
index f07773f8bd..921433cadd 100644
--- a/test-suite/success/ImplicitArguments.v
+++ b/test-suite/success/ImplicitArguments.v
@@ -27,3 +27,8 @@ Parameters (a:_) (b:a=0).
 Definition foo6 (x:=1) : forall {n:nat}, n=n := fun n => eq_refl.
 
 Fixpoint foo7 (x:=1) (n:nat) {p:nat} {struct n} : nat.
+
+(* Some example which should succeed with local implicit arguments *)
+
+Inductive A {P:forall m {n}, n=m -> Prop} := C : P 0 eq_refl -> A.
+Inductive B (P:forall m {n}, n=m -> Prop) := D : P 0 eq_refl -> B P.
diff --git a/test-suite/success/Record.v b/test-suite/success/Record.v
index 8334322c99..6f27c1d369 100644
--- a/test-suite/success/Record.v
+++ b/test-suite/success/Record.v
@@ -87,3 +87,8 @@ Record R : Type := {
   P (A : Type) : Prop := exists x : A -> A, x = x;
   Q A : P A -> P A
 }.
+
+(* We allow reusing an implicit parameter named in non-recursive types *)
+(* This is used in a couple of development such as UniMatch *)
+
+Record S {A:Type} := { a : A; b : forall A:Type, A }.
diff --git a/test-suite/success/Scopes.v b/test-suite/success/Scopes.v
index 43e3493c1e..ca37467166 100644
--- a/test-suite/success/Scopes.v
+++ b/test-suite/success/Scopes.v
@@ -20,3 +20,9 @@ Inductive U := A.
 Bind Scope u with U.
 Notation "'ε'" := A : u.
 Definition c := ε : U.
+
+(* Check activation of type scope for tactics such as assert *)
+
+Goal True.
+assert (nat * nat).
+
diff --git a/test-suite/success/coindprim.v b/test-suite/success/coindprim.v
index 5b9265b6a8..05ab913932 100644
--- a/test-suite/success/coindprim.v
+++ b/test-suite/success/coindprim.v
@@ -13,9 +13,10 @@ Definition eta {A} (s : Stream A) := {| hd := s.(hd); tl := s.(tl) |}.
 CoFixpoint ones := {| hd := 1; tl := ones |}.
 CoFixpoint ticks := {| hd := tt; tl := ticks |}.
 
-CoInductive stream_equiv {A} {s : Stream A} {s' : Stream A} : Prop :=
-  mkStreamEq { hdeq : s.(hd) = s'.(hd); tleq : stream_equiv _ s.(tl) s'.(tl) }.
-Arguments stream_equiv {A} s s'.
+CoInductive stream_equiv {A} (s : Stream A) (s' : Stream A) : Prop :=
+  mkStreamEq { hdeq : s.(hd) = s'.(hd); tleq : stream_equiv s.(tl) s'.(tl) }.
+Arguments hdeq {A} {s} {s'}.
+Arguments tleq {A} {s} {s'}.
 
 Program CoFixpoint ones_eq : stream_equiv ones ones.(tl) :=
   {| hdeq := eq_refl; tleq := ones_eq |}.
@@ -88,4 +89,4 @@ Lemma eq (x : U) : x = force x.
 Proof.
   Fail destruct x.
 Abort.
-  (* Impossible *)
-\ No newline at end of file
+  (* Impossible *)
diff --git a/test-suite/success/evars.v b/test-suite/success/evars.v
index 4e2bf45118..82f726fa7c 100644
--- a/test-suite/success/evars.v
+++ b/test-suite/success/evars.v
@@ -62,7 +62,7 @@ Check
 
 Check (fun f:(forall (v:Type->Type), v (v nat) -> nat) => f _ (Some (Some O))).
 
-(* This used to fail with anomaly (Pp.str "evar was not declared") in V8.0pl3 *)
+(* This used to fail with anomaly (Pp.str "evar was not declared.") in V8.0pl3 *)
 
 Theorem contradiction : forall p, ~ p -> p -> False.
 Proof. trivial. Qed.
diff --git a/test-suite/success/forward.v b/test-suite/success/forward.v
new file mode 100644
index 0000000000..0ed5b524f3
--- /dev/null
+++ b/test-suite/success/forward.v
@@ -0,0 +1,18 @@
+(* Testing forward reasoning *)
+
+Goal 0=0.
+Fail assert (_ = _).
+eassert (_ = _)by reflexivity.
+eassumption.
+Qed.
+
+Goal 0=0.
+Fail set (S ?[nl]).
+eset (S ?[n]).
+remember (S ?n) as x.
+instantiate (n:=0).
+Fail remember (S (S _)).
+eremember (S (S ?[x])).
+instantiate (x:=0).
+reflexivity.
+Qed.
diff --git a/test-suite/success/specialize.v b/test-suite/success/specialize.v
index 4b41a509e5..f12db8b081 100644
--- a/test-suite/success/specialize.v
+++ b/test-suite/success/specialize.v
@@ -17,6 +17,29 @@ specialize (eq_trans (x:=a)(y:=b)). intros _.
 specialize (eq_trans H H0). intros _.
 specialize (eq_trans H0 (z:=b)). intros _.
 
+(* incomplete bindings: y is left quantified and z is instantiated. *)
+specialize eq_trans with (x:=a)(z:=c).
+intro h.
+(* y can be instantiated now *)
+specialize h with (y:=b).
+(* z was instantiated above so this must fail. *)
+Fail specialize h with (z:=c).
+clear h.
+
+(* incomplete bindings: 1st dep hyp is instantiated thus A, x and y
+   instantiated too. *)
+specialize eq_trans with (1:=H).
+intro h.
+(* 2nd dep hyp can be instantiated now, which instatiates z too. *)
+specialize h with (1:=H0).
+(* checking that there is no more products in h. *)
+match type of h with
+| _ = _ => idtac
+| _ => fail "specialize test failed: hypothesis h should be an equality at this point"
+end.
+clear h.
+
+
 (* local "in place" specialization *)
 assert (Eq:=eq_trans).
 
@@ -31,6 +54,27 @@ specialize (Eq _ a b c). Undo.
 specialize (Eq _ _ _ _ H H0). Undo.
 specialize (Eq _ _ _ b H0). Undo.
 
+(* incomplete binding *)
+specialize Eq with (y:=b).
+(* A and y have been instantiated so this works *)
+specialize (Eq _ _ H H0).
+Undo 2.
+
+(* incomplete binding (dependent) *)
+specialize Eq with (1:=H).
+(* A, x and y have been instantiated so this works *)
+specialize (Eq _ H0).
+Undo 2.
+
+(* incomplete binding (dependent) *)
+specialize Eq with (1:=H) (2:=H0).
+(* A, x and y have been instantiated so this works *)
+match type of Eq with
+| _ = _ => idtac
+| _ => fail "specialize test failed: hypothesis Eq should be an equality at this point"
+end.
+Undo 2.
+
 (*
 (** strange behavior to inspect more precisely *)
 
@@ -40,7 +84,7 @@ specialize (Eq _ _ _ b H0). Undo.
 (* 2) echoue moins lorsque zero premise de mangé *)
 specialize eq_trans with (1:=Eq).  (* mal typé !! *)
 
-(* 3) *)
+(* 3) Seems fixed.*)
 specialize eq_trans with _ a b c. intros _.
 (* Anomaly: Evar ?88 was not declared. Please report. *)
 *)