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

3 files changed, 14 insertions, 5 deletions

diff --git a/test-suite/output/Match_subterm.out b/test-suite/output/Match_subterm.out
new file mode 100644
index 000000000..951a98db0
--- /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 000000000..2c44b1879
--- /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 3bc9c7f9e..082cbfbe1 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