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

7 files changed, 27 insertions, 16 deletions

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 338f4092a2..90034e4971 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -1093,20 +1093,27 @@ let rec extern inctx scopes vars r =
 
   | RCases (loc,(typopt,rtntypopt),tml,eqns) ->
       let pred = option_app (extern_type scopes vars) typopt in
-      let rtntypopt = option_app (extern_type scopes vars) !rtntypopt in
       let vars' = 
 	List.fold_right (name_fold Idset.add)
 	  (cases_predicate_names tml) vars in
+      let rtntypopt' = option_app (extern_type scopes vars') !rtntypopt in
       let tml = List.map (fun (tm,{contents=(na,x)}) ->
+        let na' = match na,tm with
+            Anonymous, RVar (_,id) when 
+              !rtntypopt<>None & occur_rawconstr id (out_some !rtntypopt)
+              -> Some Anonymous
+          | Anonymous, _ -> None
+          | Name id, RVar (_,id') when id=id' -> None
+          | Name _, _ -> Some na in
 	(sub_extern false scopes vars tm,
-	(na,option_app (fun (loc,ind,nal) ->
+	(na',option_app (fun (loc,ind,nal) ->
 	  let args = List.map (function
 	    | Anonymous -> RHole (dummy_loc,InternalHole) 
 	    | Name id -> RVar (dummy_loc,id)) nal in
 	  let t = RApp (dummy_loc,RRef (dummy_loc,IndRef ind),args) in
 	  (extern_type scopes vars t)) x))) tml in
       let eqns = List.map (extern_eqn (typopt<>None) scopes vars) eqns in 
-      CCases (loc,(pred,rtntypopt),tml,eqns)
+      CCases (loc,(pred,rtntypopt'),tml,eqns)
 
   | ROrderedCase (loc,cs,typopt,tm,bv,{contents = Some x}) ->
       extern false scopes vars x
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 19a705ec30..53e6867057 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -743,8 +743,9 @@ let internalise sigma env allow_soapp lvar c =
     | None -> 
 	ids, None in
     let na = match tm, na with
-      | RVar (_,id), Anonymous when Idset.mem id vars -> Name id
-      | _ -> na in
+      | RVar (_,id), None when Idset.mem id vars & not !Options.v7 -> Name id
+      | _, None -> Anonymous
+      | _, Some na -> na in
     (na,typ), name_fold Idset.add na ids
 
   and iterate_prod loc2 env ty body = function
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index 23268556a8..3e4d3684d0 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -348,7 +348,7 @@ type constr_expr =
   | CApp of loc * (proj_flag * constr_expr) * 
       (constr_expr * explicitation located option) list
   | CCases of loc * (constr_expr option * constr_expr option) *
-      (constr_expr * (name * constr_expr option)) list *
+      (constr_expr * (name option * constr_expr option)) list *
       (loc * cases_pattern_expr list * constr_expr) list
   | COrderedCase of loc * case_style * constr_expr option * constr_expr
       * constr_expr list
@@ -507,7 +507,8 @@ let map_constr_expr_with_binders f g e = function
 	    option_fold_right
 	      (fun t ->
 		let ids = names_of_cases_indtype t in
-		List.fold_right g ids) indnal (name_fold g na e))
+		List.fold_right g ids)
+            indnal (option_fold_right (name_fold g) na e))
 	  a e
       in
       CCases (loc,(option_app (f e) po, option_app (f e') rtnpo),
diff --git a/interp/topconstr.mli b/interp/topconstr.mli
index d782a4fdcf..241d84687f 100644
--- a/interp/topconstr.mli
+++ b/interp/topconstr.mli
@@ -89,7 +89,7 @@ type constr_expr =
   | CApp of loc * (proj_flag * constr_expr) * 
         (constr_expr * explicitation located option) list
   | CCases of loc * (constr_expr option * constr_expr option) *
-      (constr_expr * (name * constr_expr option)) list *
+      (constr_expr * (name option * constr_expr option)) list *
       (loc * cases_pattern_expr list * constr_expr) list
   | COrderedCase of loc * case_style * constr_expr option * constr_expr
       * constr_expr list
diff --git a/parsing/g_cases.ml4 b/parsing/g_cases.ml4
index 2c5640d181..56c5229488 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 8aebc87bb4..cf7dafb47b 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];
diff --git a/translate/ppconstrnew.ml b/translate/ppconstrnew.ml
index af8fb845de..8104399c0b 100644
--- a/translate/ppconstrnew.ml
+++ b/translate/ppconstrnew.ml
@@ -351,12 +351,17 @@ let tm_clash = function
 
 let pr_case_item pr (tm,(na,indnalopt)) =
   hov 0 (pr (lcast,E) tm ++
+(*
   (match na with
     | Name id when not (is_var id tm) -> spc () ++ str "as " ++  pr_id id
     | Anonymous when tm_clash (tm,indnalopt) <> None ->
 	(* hide [tm] name to avoid conflicts *)
 	spc () ++ str "as _" (* ++ pr_id (out_some (tm_clash (tm,indnalopt)))*)
     | _ -> mt ()) ++
+*)
+  (match na with (* Decision of printing "_" or not moved to constrextern.ml *)
+    | Some na -> spc () ++ str "as " ++  pr_name na
+    | None -> mt ()) ++
   (match indnalopt with
     | None -> mt ()
 (*