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 /parsing | |
| 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 'parsing')
| -rw-r--r-- | parsing/g_ltac.ml4 | 4 | ||||
| -rw-r--r-- | parsing/pptactic.ml | 2 | ||||
| -rw-r--r-- | parsing/q_coqast.ml4 | 4 |
3 files changed, 5 insertions, 5 deletions
diff --git a/parsing/g_ltac.ml4 b/parsing/g_ltac.ml4 index d9bc8038b9..f869dc8e8d 100644 --- a/parsing/g_ltac.ml4 +++ b/parsing/g_ltac.ml4 @@ -72,10 +72,10 @@ GEXTEND Gram | ta0 = tactic_expr; "||"; ta1 = tactic_expr -> TacOrelse (ta0,ta1) ] | "1" RIGHTA [ b = match_key; IDENT "goal"; "with"; mrl = match_context_list; "end" -> - TacMatchContext (b,false,mrl) + TacMatchGoal (b,false,mrl) | b = match_key; IDENT "reverse"; IDENT "goal"; "with"; mrl = match_context_list; "end" -> - TacMatchContext (b,true,mrl) + TacMatchGoal (b,true,mrl) | b = match_key; c = tactic_expr; "with"; mrl = match_list; "end" -> TacMatch (b,c,mrl) | IDENT "first" ; "["; l = LIST0 tactic_expr SEP "|"; "]" -> diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml index 8d1dbf8756..933667ce32 100644 --- a/parsing/pptactic.ml +++ b/parsing/pptactic.ml @@ -899,7 +899,7 @@ let rec pr_tac inherited tac = lrul ++ fnl() ++ str "end"), lmatch - | TacMatchContext (lz,lr,lrul) -> + | TacMatchGoal (lz,lr,lrul) -> hov 0 (pr_lazy lz ++ str (if lr then "match reverse goal with" else "match goal with") ++ prlist diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4 index 56afbc9bee..113e88cd35 100644 --- a/parsing/q_coqast.ml4 +++ b/parsing/q_coqast.ml4 @@ -470,8 +470,8 @@ and mlexpr_of_tactic : (Tacexpr.raw_tactic_expr -> MLast.expr) = function $mlexpr_of_bool lz$ $mlexpr_of_tactic t$ $mlexpr_of_list (mlexpr_of_match_rule mlexpr_of_tactic) l$>> - | Tacexpr.TacMatchContext (lz,lr,l) -> - <:expr< Tacexpr.TacMatchContext + | Tacexpr.TacMatchGoal (lz,lr,l) -> + <:expr< Tacexpr.TacMatchGoal $mlexpr_of_bool lz$ $mlexpr_of_bool lr$ $mlexpr_of_list (mlexpr_of_match_rule mlexpr_of_tactic) l$>> |