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

1 files changed, 2 insertions, 2 deletions

diff --git a/theories/Init/Tactics.v b/theories/Init/Tactics.v
index f0a17d7a4..705fb3bdf 100644
--- a/theories/Init/Tactics.v
+++ b/theories/Init/Tactics.v
@@ -115,7 +115,7 @@ lazymatch T with
     evar (a : t); pose proof (H a) as H1; unfold a in H1;
     clear a; clear H; rename H1 into H; find_equiv H
 | ?A <-> ?B => idtac
-| _ => fail "The given statement does not seem to end with an equivalence."
+| _ => fail "The given statement does not seem to end with an equivalence"
 end.
 
 Ltac bapply lemma todo :=
@@ -141,7 +141,7 @@ t;
 match goal with
 | H : _ |- _ => solve [inversion H]
 | _ => solve [trivial | reflexivity | symmetry; trivial | discriminate | split]
-| _ => fail 1 "Cannot solve this goal."
+| _ => fail 1 "Cannot solve this goal"
 end.
 
 (** A tactic to document or check what is proved at some point of a script *)