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

4 files changed, 17 insertions, 8 deletions

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 338f4092a..90034e497 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 19a705ec3..53e686705 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 23268556a..3e4d3684d 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 d782a4fdc..241d84687 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