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
---
 contrib/interface/depends.ml | 2 +-
 contrib/interface/xlate.ml   | 6 +++---
 2 files changed, 4 insertions(+), 4 deletions(-)

(limited to 'contrib/interface')

diff --git a/contrib/interface/depends.ml b/contrib/interface/depends.ml
index bf1cf5e7b2..203bc9e3dd 100644
--- a/contrib/interface/depends.ml
+++ b/contrib/interface/depends.ml
@@ -268,7 +268,7 @@ let rec depends_of_gen_tactic_expr depends_of_'constr depends_of_'ind depends_of
 	     igtal
 	     acc)
     | TacMatch (_, tac, tacexpr_mrl) -> failwith "depends_of_tacexpr of a Match not implemented yet"
-    | TacMatchContext (_, _, tacexpr_mrl) -> failwith "depends_of_tacexpr of a Match Context not implemented yet"
+    | TacMatchGoal (_, _, tacexpr_mrl) -> failwith "depends_of_tacexpr of a Match Context not implemented yet"
     | TacFun tacfa -> depends_of_tac_fun_ast tacfa acc
     | TacArg tacarg -> depends_of_tac_arg tacarg acc
   and depends_of_atomic_tacexpr atexpr acc = let depends_of_'constr_with_bindings = depends_of_'a_with_bindings depends_of_'constr in match atexpr with
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index 716f6da3b7..e368ff637e 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -830,11 +830,11 @@ and xlate_tactic =
                          | [] -> assert false
                          | fst::others ->
                              CT_match_tac_rules(fst, others))
-   | TacMatchContext (_,_,[]) | TacMatchContext (true,_,_) -> failwith ""
-   | TacMatchContext (false,false,rule1::rules) ->
+   | TacMatchGoal (_,_,[]) | TacMatchGoal (true,_,_) -> failwith ""
+   | TacMatchGoal (false,false,rule1::rules) ->
          CT_match_context(xlate_context_rule rule1,
                           List.map xlate_context_rule rules)
-   | TacMatchContext (false,true,rule1::rules) ->
+   | TacMatchGoal (false,true,rule1::rules) ->
          CT_match_context_reverse(xlate_context_rule rule1,
                           List.map xlate_context_rule rules)
    | TacLetIn (false, l, t) ->
-- 
cgit v1.2.3