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

2 files changed, 19 insertions, 24 deletions

diff --git a/syntax/PPCases.v b/syntax/PPCases.v
index f8b4eb9475..ff2aca9b39 100644
--- a/syntax/PPCases.v
+++ b/syntax/PPCases.v
@@ -78,8 +78,6 @@ Syntax constr
   | let_binder_tail_cons [ << (LETBINDERTAIL $var ($LIST $vars)) >> ]
       -> [ "," [1 0] $var (LETBINDERTAIL ($LIST $vars)) ]
 
-  | elim_pred      [ << (ELIMPRED $pred) >> ]          -> [ "<" $pred:E ">" [0 2] ]
-  | elim_pred_xtra [ << (ELIMPRED "SYNTH") >> ] -> [ ]
   ;
 
   (* On force les parenthèses autour d'un "if" sous-terme (même si le
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: