diff options
| author |  delahaye <delahaye@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-04-13 18:34:55 +0000 |
|---|---|---|
| committer | delahaye <delahaye@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-04-13 18:34:55 +0000 |
| commit | 989e3d5eb6c6f9f07b95ae40e655d72a7af9dbc1 (patch) | |
| tree | 5b8ecf10a0fb4ab5c638998534315f20ec840d50 /syntax | |
| parent | a8dddac7d3c13a902da81b1521dedc245f485243 (diff) | |
Reparation de l'affichage des THEN's
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1588 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'syntax')
| -rw-r--r-- | syntax/PPTactic.v | 26 |
1 files changed, 11 insertions, 15 deletions
diff --git a/syntax/PPTactic.v b/syntax/PPTactic.v index bdedb15c6..4b4c7ddcf 100644 --- a/syntax/PPTactic.v +++ b/syntax/PPTactic.v @@ -17,18 +17,18 @@ Syntax tactic interpret [<<(Interp (TACTIC $t))>>] -> [ $t:E ] ; - (* Put parenthesis when there is more than one tactic *) level 3: - tacsemilist_many [<<(TACTICLIST ($LIST $L))>>] - -> [ [ <hov 2> (TACTICS ($LIST $L)) ] ] + | tacticlist_parsimp [<<(TACTICLISTPAR $tac0 $tac1)>>] -> + [ $tac0 ";" [1 0] $tac1] + | tacticlist_parcomp [<<(TACTICLISTPAR $tac0 (TACTICLIST $tac1 $tac2))>>] + -> [ (TACTICLIST $tac0 (TACTICLIST $tac1 $tac2)) ] ; level 2: - tacsemilist_one [<<(TACTICLIST $tac)>>] -> [(TACTICS $tac)] - | tacticlist_cons [<<(TACTICS $t1 ($LIST $l))>>] - -> [ [<hov 0> $t1:E] ";" [1 0] (TACTICS ($LIST $l)) ] - | tacticlist_one [<<(TACTICS $t1)>>] -> [ [<hov 0> $t1:E] ] - + | tacticlist_simp [<<(TACTICLIST $tac0 $tac1)>>] -> + [ $tac0 ";" [1 0] $tac1] + | tacticlist_comp [<<(TACTICLIST $tac0 (TACTICLIST $tac1 $tac2))>>] -> + [ $tac0 ";" [1 0] [<hov 0> (TACTICLISTPAR $tac1 $tac2):E] ] | tactic_seq [<<(TACLIST ($LIST $l))>>] -> [ [<hv 0> "[ " (TACTICSEQBODY ($LIST $l)) " ]" ] ] | tacticseqbody_cons [<<(TACTICSEQBODY $t ($LIST $l))>>] @@ -59,8 +59,6 @@ Syntax tactic level 1: orelse [ $st Orelse $tc ] -> [ [<hov 0> $st:L " Orelse" [1 1] $tc:E] ] - -(* orelse [ (ORELSE $st $tc)>>] -> [ [<hov 0> $st:L " Orelse" [1 1] $tc:E] ]*) ; level 0: @@ -69,7 +67,9 @@ Syntax tactic (* PP rules for LTAC *) (* ============================= *) - do [<<(DO ($NUM $n) $tc)>>] -> ["Do " $n " " $tc:E] + | idtac [<<(IDTAC)>>] -> ["Idtac"] + | fail [<<(FAIL)>>] -> ["Fail"] + | do [<<(DO ($NUM $n) $tc)>>] -> ["Go " $n " " $tc:E] | try [<<(TRY $t)>>] -> ["Try " $t:E] | info [<<(INFO $t)>>] -> ["Info " $t:E] | repeat [<<(REPEAT $tc)>>] -> ["Repeat " $tc:E] @@ -206,9 +206,6 @@ Syntax tactic | symmetry [<<(Symmetry)>>] -> ["Symmetry"] | transitivity [<<(Transitivity $C)>>] -> ["Transitivity " $C] - | idtac [<<(Idtac)>>] -> ["Idtac"] - - (* ============================================== *) (* PP rules for tactic arguments *) (* ============================================== *) @@ -359,4 +356,3 @@ Syntax tactic | tactic_qualidarg_nil [<<(QUALIDARG $id)>>] -> [ $id ] | tactic_qualidarg_cons [<<(QUALIDARG $id $p)>>] -> [ $id [1 0] "." (QUALID $p) ]. - |