diff options
| author |  delahaye <delahaye@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-05-27 15:35:34 +0000 |
|---|---|---|
| committer | delahaye <delahaye@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-05-27 15:35:34 +0000 |
| commit | 34e53d5418fa08e69c8f599bb55a89eae027b9b5 (patch) | |
| tree | 7d3b8df0513be3885aedc9b65ff18167ca77a530 /syntax | |
| 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 'syntax')
| -rw-r--r-- | syntax/PPTactic.v | 19 |
1 files changed, 14 insertions, 5 deletions
diff --git a/syntax/PPTactic.v b/syntax/PPTactic.v index 05effb243..434590cb8 100644 --- a/syntax/PPTactic.v +++ b/syntax/PPTactic.v @@ -42,7 +42,7 @@ Syntax tactic level 2: | orelse [ $st Orelse $tc ] -> [ [<hov 0> $st:L " Orelse" [1 1] $tc:E] ] - | match_context [<<(MATCHCONTEXT ($LIST $lrul))>>] -> + | match_context [<<(MATCHCONTEXT "RL" ($LIST $lrul))>>] -> [ [ <hov 0> "Match Context With" (MATCHCONTEXTLIST ($LIST $lrul)) ] ] | match [<<(MATCH $t ($LIST $lrul))>>] -> [ [ <hov 0> "Match" [1 0] $t [1 0] "With" (MATCHLIST ($LIST $lrul)) ] ] @@ -138,10 +138,13 @@ Syntax tactic ["First" [1 0] "[" [1 0] (TACTICSEQBODY ($LIST $l)) [1 0] "]"] | solve [<<(TCLSOLVE ($LIST $l))>>] -> ["Solve" [1 0] "[" [1 0] (TACTICSEQBODY ($LIST $l)) [1 0] "]"] - | abstract_anon [<<(ABSTRACT (TACTIC $t))>>] - -> ["Abstract " $t:E] - | abstract_name [<<(ABSTRACT ($VAR $id) (TACTIC $t))>>] - -> ["Abstract " $t:E " using " $id] + | abstract_anon [<<(ABSTRACT (TACTIC $t))>>] -> ["Abstract " $t:E] + | abstract_name [<<(ABSTRACT ($VAR $id) (TACTIC $t))>>] -> + ["Abstract " $t:E " using " $id] + | eval [<<(EVAL $c (REDEXP $rtc))>>] -> + ["Eval" [1 0] (REDEXP $rtc) [1 0] "in" [1 0] (COMMAND $c)] + | inst [<<(CONTEXT $id $c)>>] -> ["Inst" [1 0] $id "[" (COMMAND $c) "]"] + | check [<<(CHECK $c)>>] -> ["Check" [1 0] (COMMAND $c)] (* =================================== *) (* PP rules for simple tactics *) @@ -434,6 +437,12 @@ Syntax tactic | tactic_to_castedconstr [<<(CASTEDCOMMAND $c)>>] -> [ $c:"constr":9 ] | tactic_to_openconstr [<<(CASTEDOPENCOMMAND $c)>>] -> [ $c:"constr":9 ] + (* Some operations over constr to be pretty-printed here *) + | eval_command [<<(COMMAND (EVAL $c (REDEXP $rtc)))>>] -> + [(EVAL $c (REDEXP $rtc))] + | inst_command [<<(COMMAND (CONTEXT $id $c))>>] -> [(CONTEXT $id $c)] + | check_command [<<(COMMAND (CHECK $c))>>] -> [(CHECK $c)] + (* This is produced bu UNFOLDLIST *) | tactic_qualidarg_constr [<<(COMMAND (QUALIDARG $p))>>] -> [(QUALIDARG $p)] | tactic_qualidarg_nil [<<(QUALIDARG $id)>>] -> [ $id ] |