diff options
| author | herbelin | 2001-10-05 14:30:35 +0000 |
|---|---|---|
| committer | herbelin | 2001-10-05 14:30:35 +0000 |
| commit | b35f7449426057e962d5646a216dbc63df33a046 (patch) | |
| tree | c61b75f1ba2cb292556d6d7d3f66846c5fb845c6 /parsing | |
| parent | 4e81371e3c5e0c91c79c8b78b8711309932e3a60 (diff) | |
Nouvelle tactique primitive ThinBody et nouvelles tactiques utilisateurs 'ClearBody H' et 'Assert H := c'
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2104 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/g_tactic.ml4 | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4 index ea227c1122..21e151c11e 100644 --- a/parsing/g_tactic.ml4 +++ b/parsing/g_tactic.ml4 @@ -318,6 +318,11 @@ GEXTEND Gram | Coqast.Node(_,"COMMAND",[c]) -> coerce_to_var c | _ -> assert false in <:ast< (TrueCut $t $id) >> + | IDENT "Assert"; c = constrarg; ":="; t = constrarg -> + let id = match c with + | Coqast.Node(_,"COMMAND",[c]) -> coerce_to_var c + | _ -> assert false in + <:ast< (Forward $t $id) >> | IDENT "Specialize"; n = pure_numarg; lcb = constrarg_binding_list -> <:ast< (Specialize $n ($LIST $lcb))>> | IDENT "Specialize"; lcb = constrarg_binding_list -> @@ -331,6 +336,8 @@ GEXTEND Gram | IDENT "LApply"; c = constrarg -> <:ast< (CutAndApply $c) >> | IDENT "Clear"; l = ne_idmetahyp_list -> <:ast< (Clear (CLAUSE ($LIST $l))) >> + | IDENT "ClearBody"; l = ne_idmetahyp_list -> + <:ast< (ClearBody (CLAUSE ($LIST $l))) >> | IDENT "Move"; id1 = identarg; IDENT "after"; id2 = identarg -> <:ast< (MoveDep $id1 $id2) >> (*To do: put Abstract in Refiner*) |