Imported Upstream version 8.3upstream/8.3

3 files changed, 61 insertions, 0 deletions

diff --git a/test-suite/success/implicit.v b/test-suite/success/implicit.v
index 59e1a935..ce3e692f 100644
--- a/test-suite/success/implicit.v
+++ b/test-suite/success/implicit.v
@@ -86,3 +86,24 @@ Fixpoint plus n m {struct n} :=
   | 0 => m
   | S p => S (plus p m)
   end.
+
+(* Check multiple implicit arguments signatures *)
+
+Implicit Arguments eq_refl [[A] [x]] [[A]].
+
+Check eq_refl : 0 = 0.
+
+(* Check that notations preserve implicit (since 8.3) *)
+
+Parameter p : forall A, A -> forall n, n = 0 -> True.
+Implicit Arguments p [A n].
+Notation Q := (p 0).
+Check Q eq_refl.
+
+(* Check implicits with Context *)
+
+Section C.
+Context {A:Set}.
+Definition h (a:A) := a.
+End C.
+Check h 0.
diff --git a/test-suite/success/ltac.v b/test-suite/success/ltac.v
index dfa41c82..02618c2c 100644
--- a/test-suite/success/ltac.v
+++ b/test-suite/success/ltac.v
@@ -243,3 +243,35 @@ test_open_match (forall z y, y + z  = 0).
 reflexivity.
 apply I.
 Qed.
+
+(* Test regular failure when clear/intro breaks soundness of the
+   interpretation of terms in current environment *)
+
+Ltac g y := clear y; assert (y=y).
+Goal forall x:nat, True.
+intro x.
+Fail g x.
+Abort.
+
+Ltac h y := assert (y=y).
+Goal forall x:nat, True.
+intro x.
+Fail clear x; f x.
+Abort.
+
+(* Do not consider evars as unification holes in Ltac matching (and at
+   least not as holes unrelated to the original evars)
+   [Example adapted from Ynot code]
+ *)
+
+Ltac not_eq e1 e2 :=
+  match e1 with
+    | e2 => fail 1
+    | _ => idtac
+  end.
+
+Goal True.
+evar(foo:nat).
+let evval := eval compute in foo in not_eq evval 1.
+let evval := eval compute in foo in not_eq 1 evval.
+Abort.
diff --git a/test-suite/success/unfold.v b/test-suite/success/unfold.v
index 47ca0836..5649e2f7 100644
--- a/test-suite/success/unfold.v
+++ b/test-suite/success/unfold.v
@@ -13,3 +13,11 @@ Goal EQ nat 0 0.
 Hint Unfold EQ.
 auto.
 Qed.
+
+(* Check regular failure when statically existing ref does not exist
+   any longer at run time *)
+
+Goal let x := 0 in True.
+intro x.
+Fail (clear x; unfold x).
+Abort.