From 04fb64e05365cb6eaf56baeffc72aa0b5d4b9a1b Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 5 Aug 2008 15:38:31 +0000
Subject: Correction de bugs: - evarconv: mauvaise idée d'utiliser la
 conversion sur la tête d'un   terme applicatif au moment de tester f u1 .. un
 = g v1 .. vn au   premier ordre : on revient sur l'algo tel qu'il était avant
 le   commit 11187. - Bug #1887 (format récursif cassé à cause de la
 vérification des idents). - Nouveau choix de formattage du message "Tactic
 Failure". - Nettoyage vocabulaire "match context" -> "match goal" au passage.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11305 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 test-suite/output/Match_subterm.out | 8 ++++++++
 test-suite/output/Match_subterm.v   | 6 ++++++
 test-suite/success/evars.v          | 5 -----
 3 files changed, 14 insertions(+), 5 deletions(-)
 create mode 100644 test-suite/output/Match_subterm.out
 create mode 100644 test-suite/output/Match_subterm.v

(limited to 'test-suite')

diff --git a/test-suite/output/Match_subterm.out b/test-suite/output/Match_subterm.out
new file mode 100644
index 0000000000..951a98db0e
--- /dev/null
+++ b/test-suite/output/Match_subterm.out
@@ -0,0 +1,8 @@
+(0 = 1)
+eq
+nat
+0
+1
+S
+0
+2
diff --git a/test-suite/output/Match_subterm.v b/test-suite/output/Match_subterm.v
new file mode 100644
index 0000000000..2c44b1879f
--- /dev/null
+++ b/test-suite/output/Match_subterm.v
@@ -0,0 +1,6 @@
+Goal 0 = 1.
+match goal with
+| |- context [?v] =>
+  idtac v ; fail
+| _ => idtac 2
+end.
diff --git a/test-suite/success/evars.v b/test-suite/success/evars.v
index 3bc9c7f9e1..082cbfbe17 100644
--- a/test-suite/success/evars.v
+++ b/test-suite/success/evars.v
@@ -198,11 +198,6 @@ Goal forall x : nat, F1 x -> G1 x.
 refine (fun x H => proj2 (_ x H) _).
 Abort.
 
-(* First-order unification between beta-redex (is it useful ?) *)
-
-Check fun (y: (forall x:((fun y:Type => bool) nat), True))
-          (z: (fun z:Type => bool) _) => y z.
-
 (* Remark: the following example does not succeed any longer in 8.2 because,
    the algorithm is more general and does exclude a solution that it should
    exclude for typing reason. Handling of types and backtracking is still to
-- 
cgit v1.2.3