diff options
| author | delahaye | 2002-05-27 15:35:34 +0000 |
|---|---|---|
| committer | delahaye | 2002-05-27 15:35:34 +0000 |
| commit | 34e53d5418fa08e69c8f599bb55a89eae027b9b5 (patch) | |
| tree | 7d3b8df0513be3885aedc9b65ff18167ca77a530 /parsing | |
| parent | f6aa950ef1d5a0ff0d649e3730ce9965c4ba03b0 (diff) | |
Ajout de Eval, Inst et Check
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2711 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/g_constr.ml4 | 5 | ||||
| -rw-r--r-- | parsing/g_ltac.ml4 | 2 |
2 files changed, 5 insertions, 2 deletions
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4 index ca5f582d9f..c93acba58b 100644 --- a/parsing/g_constr.ml4 +++ b/parsing/g_constr.ml4 @@ -56,9 +56,10 @@ GEXTEND Gram constr: [ [ c = constr8 -> c | IDENT "Inst"; id = ident; "["; c = constr8; "]" -> - <:ast< (CONTEXT $id $c) >> + <:ast<(CONTEXT $id $c)>> | IDENT "Eval"; rtc = Tactic.red_tactic; "in"; c = constr8 -> - <:ast< (EVAL $c (REDEXP $rtc)) >> ] ] + <:ast<(EVAL $c (REDEXP $rtc))>> + | IDENT "Check"; c = constr8 -> <:ast<(CHECK $c)>> ] ] ; lconstr: [ [ c = constr10 -> c ] ] diff --git a/parsing/g_ltac.ml4 b/parsing/g_ltac.ml4 index 2beb62f243..ec482d43d0 100644 --- a/parsing/g_ltac.ml4 +++ b/parsing/g_ltac.ml4 @@ -145,6 +145,7 @@ GEXTEND Gram <:ast< (COMMAND (EVAL $c (REDEXP $rtc))) >> | IDENT "Inst"; id = identarg; "["; c = Constr.constr; "]" -> <:ast< (COMMAND (CONTEXT $id $c)) >> + | IDENT "Check"; c = Constr.constr -> <:ast<(COMMAND (CHECK $c))>> | st = simple_tactic -> st | id = lqualid; la = LIST1 tactic_atom0 -> <:ast< (APP $id ($LIST $la)) >> @@ -164,6 +165,7 @@ GEXTEND Gram <:ast< (COMMAND (EVAL $c (REDEXP $rtc))) >> | IDENT "Inst"; id = identarg; "["; c = Constr.constr; "]" -> <:ast< (COMMAND (CONTEXT $id $c)) >> + | IDENT "Check"; c = Constr.constr -> <:ast<(COMMAND (CHECK $c))>> | "'"; c = constrarg -> c ] ] ; lqualid: |