diff options
| author | herbelin | 2008-08-05 15:38:31 +0000 |
|---|---|---|
| committer | herbelin | 2008-08-05 15:38:31 +0000 |
| commit | 04fb64e05365cb6eaf56baeffc72aa0b5d4b9a1b (patch) | |
| tree | 26f5008ac4e4379128854cd3396c682c06792e94 /contrib/interface | |
| parent | 93db5abc5de50a6c43e2b94915cedce29b4a9c02 (diff) | |
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
Diffstat (limited to 'contrib/interface')
| -rw-r--r-- | contrib/interface/depends.ml | 2 | ||||
| -rw-r--r-- | contrib/interface/xlate.ml | 6 |
2 files changed, 4 insertions, 4 deletions
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) -> |