From f2d06f15a11fa4261483ac59eda33fa11f784e9a Mon Sep 17 00:00:00 2001
From: clrenard
Date: Mon, 11 Jun 2001 14:45:20 +0000
Subject: 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
---
 syntax/PPCases.v  |  2 --
 syntax/PPConstr.v | 41 +++++++++++++++++++----------------------
 2 files changed, 19 insertions(+), 24 deletions(-)

(limited to 'syntax')

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:
-- 
cgit v1.2.3