diff options
| author | clrenard | 2001-06-11 14:45:20 +0000 |
|---|---|---|
| committer | clrenard | 2001-06-11 14:45:20 +0000 |
| commit | f2d06f15a11fa4261483ac59eda33fa11f784e9a (patch) | |
| tree | 8324137172a45a71e11fa53aca527840bec19765 /syntax/PPConstr.v | |
| parent | dd0cf23cd41386cf028aa212487c35f54f149e70 (diff) | |
Reparation d'un bug d'affichage. Les let destructurants, if, et vieux Case
n'etaient pas affiches correctement lors du Save si on les avait donne en
argument de tactique. Avec Bruno, nous avons simplifie l'ast en remplacant
les MLCASE NOREC et autres CASE NOREC par des choses plus simples.
Il y a maintenant un noeud LET, un IF, un CASE et un MATCH qui sont a peu pres
semblables mais qui permettent de se souvenir quoi afficher.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1781 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'syntax/PPConstr.v')
| -rwxr-xr-x | syntax/PPConstr.v | 41 |
1 files changed, 19 insertions, 22 deletions
diff --git a/syntax/PPConstr.v b/syntax/PPConstr.v index 436b2b8136..f78ef411ea 100755 --- a/syntax/PPConstr.v +++ b/syntax/PPConstr.v @@ -189,37 +189,34 @@ Syntax constr level 8: - recpr [ << (XTRA "REC" ($LIST $RECARGS)) >> ] -> [ (RECTERM ($LIST $RECARGS)) ] - - | recterm [ << (RECTERM $P $c ($LIST $BL)) >> ] -> - [ [<hov 0> [<hov 0> "<" $P:E ">" + recterm [ << (MATCH $P $c ($LIST $BL)) >> ] -> + [ [<hov 0> [<hov 0> (ELIMPRED $P) [0 2] [<hov 0> "Match" [1 1] $c:E [1 0] "with" ]] [1 3] [<hov 0> (MATCHBRANCHES ($LIST $BL)):E ] "end"] ] - | mlcasepr [ << (XTRA "MLCASE" "NOREC" ($LIST $RECARGS)) >> ] - -> [ (MLCASETERM ($LIST $RECARGS)) ] - - | mlcaseterm [ << (MLCASETERM $c ($LIST $BL)) >> ] -> - [ [<hov 0> [<hov 0> "Case" [1 1] $c:E [1 0] "of" ] - [1 3] [<hov 0> (MATCHBRANCHES ($LIST $BL)):E ]"end"] ] - - | mlmatchpr [ << (XTRA "MLCASE" "REC" ($LIST $RECARGS)) >> ] - -> [ (MLMATCHTERM ($LIST $RECARGS)) ] - - | mlmatchterm [ << (MLMATCHTERM $c ($LIST $BL)) >> ] -> - [ [<hov 0> [<hov 0> "Match" [1 1] $c:E [1 0] "with" ] - [1 3] [<hov 0> (MATCHBRANCHES ($LIST $BL)):E ] "end"] ] - - | matchbranchescons [ << (MATCHBRANCHES $B ($LIST $T)) >> ] -> [ [<hov 0> [<hov 0> $B:E ] FNL] (MATCHBRANCHES ($LIST $T)):E ] | matchbranchesnil [ << (MATCHBRANCHES) >> ] -> [ ] - | casepr [ << (MUTCASE ($LIST $MATCHARGS)) >> ] -> [ (CASETERM ($LIST $MATCHARGS)) ] - | caseterm [ << (CASETERM $P $c ($LIST $BL)) >> ] -> - [ [<hov 0> [<hov 0> "<" $P:E ">" + | caseterm [ << (CASE $P $c ($LIST $BL)) >> ] -> + [ [<hov 0> [<hov 0> (ELIMPRED $P) [0 2][<hov 0> "Case" [1 1] $c:E [1 0] "of" ]] [1 3][<hov 0> (MATCHBRANCHES ($LIST $BL)):E ] "end"] ] + + | ifterm [ << (IF $P $c $b1 $b2) >> ] -> + [ (FORCEIF $P $c (EQN $b1 JUNK) (EQN $b2 JUNK)):E ] + + | letterm [ << (LET $P $c (LAMBDALIST $_ $b)) >> ] -> + [ (LETSLAM $P $c $b) ] + | letslamend [ << (LETSLAM $P $c $b ($LIST $IDL))>> ] -> + [ (FORCELET $P $c (EQN $b (PATTCONSTRUCT JUNK ($LIST $IDL)))):E ] + | letslam [ << (LETSLAM $P $c [$ID]$b ($LIST $IDL))>> ] -> + [ (LETSLAM $P $c $b ($LIST $IDL) $ID) ] + | letslamanon [ << (LETSLAM $P $c [<>]$b ($LIST $IDL))>> ] -> + [ (LETSLAM $P $c $b ($LIST $IDL) _) ] + + | elim_pred [ << (ELIMPRED $pred) >> ] -> [ "<" $pred:E ">" [0 2] ] + | elim_pred_xtra [ << (ELIMPRED "SYNTH") >> ] -> [ ] ; level 0: |