diff options
| author | herbelin | 2007-04-28 09:34:32 +0000 |
|---|---|---|
| committer | herbelin | 2007-04-28 09:34:32 +0000 |
| commit | b61d0df2899f5de9c20ee4a2c4b79deb0714b162 (patch) | |
| tree | 6c548a7046878591025baae80b4ead8d5b349c2a /parsing | |
| parent | 2ed87ba29db49e043062e125f3783a553d550fc4 (diff) | |
Ajout de la possibilité d'utiliser les evars dans apply_in et elim_in.
Fusion des syntaxes de "apply" et "eapply". Ajout de "eapply in",
"erewrite" et "erewrite in". Correction au passage des bugs #1461 et
#1522).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9802 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/g_tactic.ml4 | 9 | ||||
| -rw-r--r-- | parsing/pptactic.ml | 10 | ||||
| -rw-r--r-- | parsing/q_coqast.ml4 | 4 |
3 files changed, 14 insertions, 9 deletions
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4 index fe21a876cf..3cbd12e539 100644 --- a/parsing/g_tactic.ml4 +++ b/parsing/g_tactic.ml4 @@ -321,7 +321,8 @@ GEXTEND Gram | IDENT "exact_no_check"; c = constr -> TacExactNoCheck c | IDENT "vm_cast_no_check"; c = constr -> TacVmCastNoCheck c - | IDENT "apply"; cl = constr_with_bindings -> TacApply cl + | IDENT "apply"; cl = constr_with_bindings -> TacApply (false,cl) + | IDENT "eapply"; cl = constr_with_bindings -> TacApply (true,cl) | IDENT "elim"; cl = constr_with_bindings; el = OPT eliminator -> TacElim (cl,el) | IDENT "elimtype"; c = constr -> TacElimType c @@ -422,8 +423,10 @@ GEXTEND Gram | IDENT "transitivity"; c = constr -> TacTransitivity c (* Equality and inversion *) - | IDENT "rewrite"; b = orient; c = constr_with_bindings ; cl = clause -> - TacRewrite (b,c,cl) + | IDENT "rewrite"; b = orient; c = constr_with_bindings ; cl = clause -> + TacRewrite (b,false,c,cl) + | IDENT "erewrite"; b = orient; c = constr_with_bindings ; cl = clause -> + TacRewrite (b,true,c,cl) | IDENT "dependent"; k = [ IDENT "simple"; IDENT "inversion" -> SimpleInversion | IDENT "inversion" -> FullInversion diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml index a70c9acdbb..9218fb816a 100644 --- a/parsing/pptactic.ml +++ b/parsing/pptactic.ml @@ -664,7 +664,9 @@ and pr_atom1 = function | TacExact c -> hov 1 (str "exact" ++ pr_constrarg c) | TacExactNoCheck c -> hov 1 (str "exact_no_check" ++ pr_constrarg c) | TacVmCastNoCheck c -> hov 1 (str "vm_cast_no_check" ++ pr_constrarg c) - | TacApply cb -> hov 1 (str "apply" ++ spc () ++ pr_with_bindings cb) + | TacApply (ev,cb) -> + hov 1 (str (if ev then "eapply" else "apply") ++ spc () ++ + pr_with_bindings cb) | TacElim (cb,cbo) -> hov 1 (str "elim" ++ pr_arg pr_with_bindings cb ++ pr_opt pr_eliminator cbo) @@ -805,9 +807,9 @@ and pr_atom1 = function | TacTransitivity c -> str "transitivity" ++ pr_constrarg c (* Equality and inversion *) - | TacRewrite (b,c,cl) -> - hov 1 (str "rewrite" ++ pr_orient b ++ spc() ++ pr_with_bindings c ++ - pr_clauses pr_ident cl) + | TacRewrite (b,ev,c,cl) -> + hov 1 (str (if ev then "erewrite" else "rewrite") ++ pr_orient b ++ + spc() ++ pr_with_bindings c ++ pr_clauses pr_ident cl) | TacInversion (DepInversion (k,c,ids),hyp) -> hov 1 (str "dependent " ++ pr_induction_kind k ++ spc () ++ pr_quantified_hypothesis hyp ++ diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4 index bea93a39c3..ef25e9b8d6 100644 --- a/parsing/q_coqast.ml4 +++ b/parsing/q_coqast.ml4 @@ -273,8 +273,8 @@ let rec mlexpr_of_atomic_tactic = function <:expr< Tacexpr.TacExactNoCheck $mlexpr_of_constr c$ >> | Tacexpr.TacVmCastNoCheck c -> <:expr< Tacexpr.TacVmCastNoCheck $mlexpr_of_constr c$ >> - | Tacexpr.TacApply cb -> - <:expr< Tacexpr.TacApply $mlexpr_of_constr_with_binding cb$ >> + | Tacexpr.TacApply (false,cb) -> + <:expr< Tacexpr.TacApply False $mlexpr_of_constr_with_binding cb$ >> | Tacexpr.TacElim (cb,cbo) -> let cb = mlexpr_of_constr_with_binding cb in let cbo = mlexpr_of_option mlexpr_of_constr_with_binding cbo in |