Distinction entre 'as _' qui cache le terme filtre (si variable) et rien dans case_item

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

2 files changed, 5 insertions, 8 deletions

diff --git a/parsing/g_cases.ml4 b/parsing/g_cases.ml4
index 2c5640d18..56c522948 100644
--- a/parsing/g_cases.ml4
+++ b/parsing/g_cases.ml4
@@ -57,17 +57,17 @@ GEXTEND Gram
   operconstr: LEVEL "1"
     [ [ "<"; p = annot; ">"; "Cases"; lc = LIST1 constr; "of";
         OPT "|"; eqs = ne_eqn_list; "end" ->
-          let lc = List.map (fun c -> c,(Names.Anonymous,None)) lc in
+          let lc = List.map (fun c -> c,(None,None)) lc in
 	  CCases (loc, (Some p,None), lc, eqs)
       | "Cases"; lc = LIST1 constr; "of";
 	OPT "|"; eqs = ne_eqn_list; "end" ->
-          let lc = List.map (fun c -> c,(Names.Anonymous,None)) lc in
+          let lc = List.map (fun c -> c,(None,None)) lc in
 	  CCases (loc, (None,None), lc, eqs)
       | "<"; p = annot; ">"; "Cases"; lc = LIST1 constr; "of"; "end" ->
-          let lc = List.map (fun c -> c,(Names.Anonymous,None)) lc in
+          let lc = List.map (fun c -> c,(None,None)) lc in
 	  CCases (loc, (Some p,None), lc, [])
       | "Cases"; lc = LIST1 constr; "of"; "end" -> 
-          let lc = List.map (fun c -> c,(Names.Anonymous,None)) lc in
+          let lc = List.map (fun c -> c,(None,None)) lc in
 	  CCases (loc, (None,None), lc, []) ] ]
   ;
 END;
diff --git a/parsing/g_constrnew.ml4 b/parsing/g_constrnew.ml4
index 8aebc87bb..cf7dafb47 100644
--- a/parsing/g_constrnew.ml4
+++ b/parsing/g_constrnew.ml4
@@ -257,10 +257,7 @@ GEXTEND Gram
         br=branches; "end" -> mk_match (loc,ci,ty,br) ] ]
   ;
   case_item:
-    [ [ c=operconstr LEVEL "100"; p=pred_pattern -> 
-        match p with
-        | (None,indp) -> (c,(Anonymous,indp))
-        | (Some na,indp) -> (c,(na,indp)) ] ]
+    [ [ c=operconstr LEVEL "100"; p=pred_pattern -> (c,p) ] ]
   ;
   pred_pattern:
     [ [ ona = OPT ["as"; id=name -> snd id];