MAJ

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

2 files changed, 26 insertions, 22 deletions

diff --git a/parsing/g_cases.ml4 b/parsing/g_cases.ml4
index a6dcbffe7..65248524e 100644
--- a/parsing/g_cases.ml4
+++ b/parsing/g_cases.ml4
@@ -2,14 +2,16 @@
 (* $Id$ *)
 
 open Pcoq
-open Command
+open Constr
 
 GEXTEND Gram
+  GLOBAL : constr1 pattern;
+
+(*
   pattern_list:
     [ [  -> []
       | p = pattern; pl = pattern_list -> p :: pl ] ]
   ;
-(*
   lsimple_pattern:
     [ [ c = simple_pattern2 -> c ] ]
   ;
@@ -18,16 +20,18 @@ GEXTEND Gram
     [ [ id = ident -> id
       | "("; p = lsimple_pattern; ")" -> p ] ]
   ;
+(*
   simple_pattern_list:
     [ [  -> []
       | p = simple_pattern; pl = simple_pattern_list ->
 	   p :: pl ] ]
   ;
+*)
   lsimple_pattern:
     [ [ id = ident; lp = ne_pattern_list ->
 	  <:ast< (PATTCONSTRUCT $id ($LIST $lp)) >>
-      | p = pattern; "as"; id = ident -> <:ast< (PATTAS $id $p)>>
-      | c1 = simple_pattern; ","; c2 = simple_pattern ->
+      | p = lsimple_pattern; "as"; id = ident -> <:ast< (PATTAS $id $p)>>
+      | c1 = lsimple_pattern; ","; c2 = lsimple_pattern ->
           <:ast< (PATTCONSTRUCT pair $c1 $c2) >>
       | "("; p = lsimple_pattern; ")" -> p ] ]
   ;
@@ -41,7 +45,7 @@ GEXTEND Gram
       | c1 = pattern -> [c1] ] ]
   ;
   equation:
-    [ [ lhs = ne_pattern_list; "=>"; rhs = command ->
+    [ [ lhs = ne_pattern_list; "=>"; rhs = constr ->
 	      <:ast< (EQN $rhs ($LIST $lhs)) >> ] ]
   ;
   ne_eqn_list:
@@ -49,17 +53,17 @@ GEXTEND Gram
       | e = equation -> [e] ] ]
   ;
 
-  command1:
-    [ [ "<"; l1 = lcommand; ">"; "Cases"; lc = ne_command_list; "of";
+  constr1:
+    [ [ "<"; l1 = lconstr; ">"; "Cases"; lc = ne_constr_list; "of";
         OPT "|"; eqs = ne_eqn_list; "end" ->
-          <:ast< (MULTCASE $l1 (TOMATCH ($LIST $lc)) ($LIST $eqs)) >>
-      | "Cases"; lc = ne_command_list; "of";
+          <:ast< (CASES $l1 (TOMATCH ($LIST $lc)) ($LIST $eqs)) >>
+      | "Cases"; lc = ne_constr_list; "of";
 	OPT "|"; eqs = ne_eqn_list; "end" ->
-          <:ast< (MULTCASE "SYNTH" (TOMATCH ($LIST $lc)) ($LIST $eqs)) >>
-      | "<"; l1 = lcommand; ">"; "Cases"; lc = ne_command_list; "of";
+          <:ast< (CASES "SYNTH" (TOMATCH ($LIST $lc)) ($LIST $eqs)) >>
+      | "<"; l1 = lconstr; ">"; "Cases"; lc = ne_constr_list; "of";
         "end" ->
-          <:ast< (MULTCASE $l1 (TOMATCH ($LIST $lc))) >>
-      | "Cases"; lc = ne_command_list; "of"; "end" -> 
-          <:ast< (MULTCASE "SYNTH" (TOMATCH ($LIST $lc))) >> ] ]
+          <:ast< (CASES $l1 (TOMATCH ($LIST $lc))) >>
+      | "Cases"; lc = ne_constr_list; "of"; "end" -> 
+          <:ast< (CASES "SYNTH" (TOMATCH ($LIST $lc))) >> ] ]
   ;
 END;
diff --git a/syntax/PPCases.v b/syntax/PPCases.v
index cbb66e1dc..b26cd5a8c 100644
--- a/syntax/PPCases.v
+++ b/syntax/PPCases.v
@@ -37,17 +37,17 @@ Syntax constr
 
   level 8:
 
-    cases_exp_none [(MULTCASE $pred $tomatch)]
+    cases_exp_none [(CASES $pred $tomatch)]
       -> [ [<hov 0> (ELIMPRED $pred)
               [<hv 0> "Cases"[1 2] $tomatch:E [1 0] "of"] [1 0] "end"] ]
 
-  | cases_exp_one [(MULTCASE $pred $tomatch $eqn)]
+  | cases_exp_one [(CASES $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 [(MULTCASE $pred $tomatch $eqn1 $eqn2 ($LIST $eqns))]
+  | cases_exp_many [(CASES $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]
@@ -73,13 +73,13 @@ Syntax constr
   level 10:
     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 ] ] ] ]
+              [<hv 0> "if " [<hov 0> $tomatch:L ]
+                      [1 0] [<hov 0> "then" [1 1] $c1:L ]
+                      [1 0] [<hov 0> "else" [1 1] $c2:L ] ] ] ]
 
   | 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 ] ]
-              [1 0] "in " [<hov 0> $c:E ] ] ]
+                      [1 1] [<hov 0> $tomatch:L ] ]
+              [1 0] "in " [<hov 0> $c:L ] ] ]
 .