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

4 files changed, 34 insertions, 40 deletions

diff --git a/parsing/astterm.ml b/parsing/astterm.ml
index 85bd1a3e5f..45b6b6ae97 100644
--- a/parsing/astterm.ml
+++ b/parsing/astterm.ml
@@ -467,13 +467,13 @@ let ast_to_rawconstr sigma env allow_soapp lvar =
 		List.map (dbrec env) tms,
 		List.map (ast_to_eqn (List.length tms) env) eqns)
 
-    | Node(loc,"CASE",Str(_,isrectag)::p::c::cl) ->
+    | Node(loc,(("CASE"|"IF"|"LET"|"MATCH")as tag), p::c::cl) ->
 	let po = match p with 
 	  | Str(_,"SYNTH") -> None 
 	  | _ -> Some(dbrec env p) in
-	let isrec = match isrectag with
-	  | "REC" -> true | "NOREC" -> false 
-	  | _ -> anomaly "ast_to: wrong REC tag in CASE" in
+	let isrec = match tag with
+	  | "MATCH" -> true | ("LET"|"CASE"|"IF") -> false 
+	  | _ -> anomaly "ast_to: wrong tag in old case expression" in
 	ROldCase (loc,isrec,po,dbrec env c,
 		  Array.of_list (List.map (dbrec env) cl))
 
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index ff4a0a7580..56779d71f0 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -92,39 +92,38 @@ GEXTEND Gram
     [ [ "<"; ":"; IDENT "ast"; ":"; "<"; c = raw_constr; ">>" -> c
       | "<"; l1 = lconstr; ">"; IDENT "Match"; c = constr; "with";
         cl = ne_constr_list; "end" ->
-          <:ast< (CASE "REC" $l1 $c ($LIST $cl)) >>
+          <:ast< (MATCH $l1 $c ($LIST $cl)) >>
       | "<"; l1 = lconstr; ">"; IDENT "Match"; c = constr; "with"; "end"
         ->
-          <:ast< (CASE "REC" $l1 $c) >>
+          <:ast< (MATCH $l1 $c) >>
       | "<"; l1 = lconstr; ">"; IDENT "Case"; c = constr; "of";
         cl = ne_constr_list; "end" ->
-          <:ast< (CASE "NOREC" $l1 $c ($LIST $cl)) >>
+          <:ast< (CASE $l1 $c ($LIST $cl)) >>
       | "<"; l1 = lconstr; ">"; IDENT "Case"; c = constr; "of"; "end" ->
-          <:ast< (CASE "NOREC" $l1 $c) >>
+          <:ast< (CASE $l1 $c) >>
       | IDENT "Case"; c = constr; "of"; cl = ne_constr_list; "end" ->
-          <:ast< (CASE "NOREC" "SYNTH" $c ($LIST $cl)) >>
+          <:ast< (CASE "SYNTH" $c ($LIST $cl)) >>
       | IDENT "Case"; c = constr; "of"; "end" ->
-          <:ast< (CASE "NOREC" "SYNTH" $c) >>
+          <:ast< (CASE "SYNTH" $c) >>
       | IDENT "Match"; c = constr; "with"; cl = ne_constr_list; "end" ->
-          <:ast< (CASE "REC" "SYNTH" $c ($LIST $cl)) >>
+          <:ast< (MATCH "SYNTH" $c ($LIST $cl)) >>
       | IDENT "let"; "("; b = ne_ident_comma_list; ")"; "=";
         c = constr; "in"; c1 = constr ->
-          <:ast< (CASE "NOREC" "SYNTH" $c (LAMBDALIST (ISEVAR)
-                   ($SLAM $b $c1))) >>
+          <:ast< (LET "SYNTH" $c (LAMBDALIST (ISEVAR) ($SLAM $b $c1))) >>
       | IDENT "let"; id1 = IDENT ; "="; c = constr; "in"; c1 = constr -> 
 	  <:ast< (LETIN $c [$id1]$c1) >>
       | IDENT "if"; c1 = constr; IDENT "then"; c2 = constr;
         IDENT "else"; c3 = constr ->
-        <:ast< ( CASE "NOREC" "SYNTH" $c1 $c2 $c3) >>
+        <:ast< ( IF "SYNTH" $c1 $c2 $c3) >>
 (* EN ATTENTE DE REMPLACER CE QUI EST DANS Program.v ... *)
       | "<"; l1 = lconstr; ">";
         IDENT "let"; "("; b = ne_ident_comma_list; ")"; "=";
         c = constr; "in"; c1 = constr ->
-         <:ast< (CASE "NOREC" $l1 $c (LAMBDALIST (ISEVAR) ($SLAM $b $c1))) >>
+         <:ast< (LET $l1 $c (LAMBDALIST (ISEVAR) ($SLAM $b $c1))) >>
       | "<"; l1 = lconstr; ">";
         IDENT "if"; c1 = constr; IDENT "then";
         c2 = constr; IDENT "else"; c3 = constr ->
-          <:ast< (CASE "NOREC" $l1 $c1 $c2 $c3) >>
+          <:ast< (IF $l1 $c1 $c2 $c3) >>
       | c = constr0 -> c ] ]
   ;
   constr2: (* ~ will be here *)
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: