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/g_constr.ml4 | |
| 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/g_constr.ml4')
| -rw-r--r-- | parsing/g_constr.ml4 | 5 |
1 files changed, 3 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 ] ] |