PPMultipleCase.v -> PPCases.v et MAJ

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@215 85f007b7-540e-0410-9357-904b9bb8a0f7

2 files changed, 15 insertions, 35 deletions

diff --git a/syntax/MakeBare.v b/syntax/MakeBare.v
index a3fe30035..8740d5a04 100644
--- a/syntax/MakeBare.v
+++ b/syntax/MakeBare.v
@@ -1,3 +1,3 @@
 Load PPCommand.
 Load PPTactic.
-Load PPMultipleCase.
+Load PPCases.
diff --git a/syntax/PPMultipleCase.v b/syntax/PPCases.v
index 51f75569e..801de0a67 100755..100644
--- a/syntax/PPMultipleCase.v
+++ b/syntax/PPCases.v
@@ -1,18 +1,5 @@
-(****************************************************************************)
-(*                 The Calculus of Inductive Constructions                  *)
-(*                                                                          *)
-(*                                Projet Coq                                *)
-(*                                                                          *)
-(*                     INRIA                        ENS-CNRS                *)
-(*              Rocquencourt                        Lyon                    *)
-(*                                                                          *)
-(*                                Coq V5.10                                 *)
-(*                              Nov 25th 1994                               *)
-(*                                                                          *)
-(****************************************************************************)
-(*                             PPMutilpleCase.v                             *)
-(****************************************************************************)
 
+(* $Id$ *)
 
 Syntax constr
   level 0:
@@ -22,7 +9,7 @@ Syntax constr
   ;
 
   level 10:
-    as_patt [(XTRA "AS" $var $patt)] -> [$patt:L" as "$var]
+    as_patt [(PATTAS $var $patt)] -> [$patt:L" as "$var]
   ;
 
   level 0:
@@ -32,13 +19,8 @@ Syntax constr
   ;
 
   level 8:
-    equation [(XTRA "EQN" $rhs ($LIST $lhs))]
+    equation [(EQN $rhs ($LIST $lhs))]
       -> [ [<hov 0> (PATTLIST ($LIST $lhs)) "=> " [0 1] $rhs:E] ]
-  | lam_eqn [(XTRA "LAMEQN" $eq)] -> [ $eq ]
-  | lam_eqn_var [(XTRA "LAMEQN" ($ID $id) ($LIST $l))]
-      -> [(XTRA "LAMEQN" ($LIST $l))]
-  | lam_eqn_dlam      [(XTRA "LAMEQN" [$_]$eq)] -> [(XTRA "LAMEQN" $eq)]
-  | lam_eqn_dlam_anon [(XTRA "LAMEQN" [<>]$eq)] -> [(XTRA "LAMEQN" $eq)]
   ;
  
   level 0:
@@ -48,22 +30,26 @@ Syntax constr
   | bar_eqnlist_one [(BAREQNLIST $eqn)]
       -> [ "| " $eqn ]
 
-  | tomatch [(XTRA "TOMATCH" ($LIST $lc))] -> [(NECOMMANDLIST2 ($LIST $lc)):E]
+  | tomatch [(TOMATCH ($LIST $lc))] -> [(NECOMMANDLIST2 ($LIST $lc)):E]
+  ;
+
+  level 10:
+    pattconstruct [(PATTCONSTRUCT ($LIST $T))] -> [(APPLIST ($LIST $T))]
   ;
 
   level 8:
 
-    cases_exp_none [(XTRA "MULTCASE" $pred $tomatch)]
+    cases_exp_none [(MULTCASE $pred $tomatch)]
       -> [ [<hov 0> (ELIMPRED $pred)
               [<hv 0> "Cases"[1 2] $tomatch:E [1 0] "of"] [1 0] "end"] ]
 
-  | cases_exp_one [(XTRA "MULTCASE" $pred $tomatch $eqn)]
+  | cases_exp_one [(MULTCASE $pred $tomatch $eqn)]
       -> [ [<hov 0> (ELIMPRED $pred)
               [<hv 0> [<hv 0> "Cases"[1 2] $tomatch:E [1 0] "of"] [1 2]
                      $eqn [1 0]
                      "end"] ] ]
 
-  | cases_exp_many [(XTRA "MULTCASE" $pred $tomatch $eqn1 $eqn2 ($LIST $eqns))]
+  | cases_exp_many [(MULTCASE $pred $tomatch $eqn1 $eqn2 ($LIST $eqns))]
       -> [ [<hov 0> (ELIMPRED $pred)
               [<v 0> [<hv 0> "Cases"[1 2] $tomatch:E [1 0] "of"] [1 2]
                      $eqn1 [1 0]
@@ -80,25 +66,19 @@ Syntax constr
       -> [ "," [1 0] $var (LETBINDERTAIL ($LIST $vars)) ]
 
   | elim_pred      [(ELIMPRED $pred)]          -> [ "<" $pred:E ">" [0 2] ]
-  | elim_pred_xtra [(ELIMPRED (XTRA"SYNTH"))] -> [ ]
+  | elim_pred_xtra [(ELIMPRED "SYNTH")] -> [ ]
   ;
 
   (* On force les parenthèses autour d'un "if" sous-terme (même si le
      parsing est lui plus tolérant) *)
   level 10:
-    boolean_cases [(FORCEIF $pred $tomatch $c1 $c2)]
+    boolean_cases [(FORCEIF $pred $tomatch (EQN $c1 $_) (EQN $c2 $_))]
       -> [ [<hov 0> (ELIMPRED $pred)
               [<hv 0> "if " [<hov 0> $tomatch:E ]
                       [1 0] [<hov 0> "then" [1 1] $c1:E ]
                       [1 0] [<hov 0> "else" [1 1] $c2:E ] ] ] ]
 
-  (* Tiens ! 
-  Pourquoi l'AST n'est pas (FORCELET $pred tomatch (EQN $c $pat)) ? 
-  Réponse : FORCELET, c'est par commodité, EQN, c'est parce qu'au parsing
-  il y a un XTRA devant **)
-
-
-  | let_cases [(XTRA "FORCELET" $pred $tomatch (XTRA "EQN" $c $pat))]
+  | let_cases [(FORCELET $pred $tomatch (EQN $c $pat))]
       -> [ [<hov 0> (ELIMPRED $pred)
               [<hv 0> "let " [<hov 0> (LETBINDER $pat) ] " ="
                       [1 1] [<hov 0> $tomatch:E ] ]