From 714849072050afc647247bb1f556c111fa4c36c5 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sun, 5 Mar 2006 09:01:05 +0000
Subject: Ajout test relatif au bug #984

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8127 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 test-suite/success/evars.v | 8 ++++++++
 test-suite/success/ltac.v  | 8 ++++++++
 2 files changed, 16 insertions(+)

diff --git a/test-suite/success/evars.v b/test-suite/success/evars.v
index ea1dd803f8..64875fbabc 100644
--- a/test-suite/success/evars.v
+++ b/test-suite/success/evars.v
@@ -60,3 +60,11 @@ Check
 (* Check instantiation of nested evars (bug #1089) *)
 
 Check (fun f:(forall (v:Set->Set), v (v nat) -> nat) => f _ (Some (Some O))).
+
+(* This used to fail with anomaly "evar was not declared" in V8.0pl3 *)
+
+Theorem contradiction : forall p, ~ p -> p -> False.
+Proof. trivial. Qed.
+Hint Resolve contradiction.
+Goal False.
+eauto.
diff --git a/test-suite/success/ltac.v b/test-suite/success/ltac.v
index b6aa1e7051..99cfe01779 100644
--- a/test-suite/success/ltac.v
+++ b/test-suite/success/ltac.v
@@ -145,3 +145,11 @@ Ltac check_binding y := cut ((fun y => y) = S).
 Goal True.
 check_binding true.
 Abort.
+
+(* Check that variables explicitly parsed as ltac variables are not
+   seen as intro pattern or constr (bug #984) *)
+
+Ltac afi tac := intros; tac.
+Goal 1 = 2.
+afi ltac:auto.
+
-- 
cgit v1.2.3