diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-04-28 09:34:32 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-04-28 09:34:32 +0000 |
| commit | b61d0df2899f5de9c20ee4a2c4b79deb0714b162 (patch) | |
| tree | 6c548a7046878591025baae80b4ead8d5b349c2a /parsing/g_tactic.ml4 | |
| 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/g_tactic.ml4')
| -rw-r--r-- | parsing/g_tactic.ml4 | 9 |
1 files changed, 6 insertions, 3 deletions
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4 index fe21a876c..3cbd12e53 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 |