Changement de l'afficheur pour que les variables liées aient un nom indépendant des globaux quand hors but (on garde l'évitement des globaux en but, pour compatibilité)

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

5 files changed, 44 insertions, 49 deletions

diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index acbdd0387e..6b091b9ced 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -164,17 +164,17 @@ let computable p k =
 let lookup_name_as_renamed env t s =
   let rec lookup avoid env_names n c = match kind_of_term c with
     | Prod (name,_,c') ->
-	(match concrete_name env avoid env_names name c' with
-           | (Some id,avoid') -> 
+	(match concrete_name true avoid env_names name c' with
+           | (Name id,avoid') -> 
 	       if id=s then (Some n) 
 	       else lookup avoid' (add_name (Name id) env_names) (n+1) c'
-	   | (None,avoid')    -> lookup avoid' env_names (n+1) (pop c'))
+	   | (Anonymous,avoid')    -> lookup avoid' env_names (n+1) (pop c'))
     | LetIn (name,_,_,c') ->
-	(match concrete_name env avoid env_names name c' with
-           | (Some id,avoid') -> 
+	(match concrete_name true avoid env_names name c' with
+           | (Name id,avoid') -> 
 	       if id=s then (Some n) 
 	       else lookup avoid' (add_name (Name id) env_names) (n+1) c'
-	   | (None,avoid')    -> lookup avoid' env_names (n+1) (pop c'))
+	   | (Anonymous,avoid')    -> lookup avoid' env_names (n+1) (pop c'))
     | Cast (c,_) -> lookup avoid env_names n c
     | _ -> None
   in lookup (ids_of_named_context (named_context env)) empty_names_context 1 t
@@ -182,20 +182,20 @@ let lookup_name_as_renamed env t s =
 let lookup_index_as_renamed env t n =
   let rec lookup n d c = match kind_of_term c with
     | Prod (name,_,c') ->
-	  (match concrete_name env [] empty_names_context name c' with
-               (Some _,_) -> lookup n (d+1) c'
-             | (None  ,_) -> if n=1 then Some d else lookup (n-1) (d+1) c')
+	  (match concrete_name true [] empty_names_context name c' with
+               (Name _,_) -> lookup n (d+1) c'
+             | (Anonymous,_) -> if n=1 then Some d else lookup (n-1) (d+1) c')
     | LetIn (name,_,_,c') ->
-	  (match concrete_name env [] empty_names_context name c' with
-             | (Some _,_) -> lookup n (d+1) c'
-             | (None  ,_) -> if n=1 then Some d else lookup (n-1) (d+1) c')
+	  (match concrete_name true [] empty_names_context name c' with
+             | (Name _,_) -> lookup n (d+1) c'
+             | (Anonymous,_) -> if n=1 then Some d else lookup (n-1) (d+1) c')
     | Cast (c,_) -> lookup n d c
     | _ -> None
   in lookup n 1 t
 
-let detype_case computable detype detype_eqn tenv avoid env indsp st p k c bl =
+let detype_case computable detype detype_eqn tenv avoid indsp st p k c bl =
   let synth_type = synthetize_type () in
-  let tomatch = detype tenv avoid env c in
+  let tomatch = detype c in
 
   (* Find constructors arity *)
   let (mib,mip) = Inductive.lookup_mind_specif tenv indsp in
@@ -209,13 +209,11 @@ let detype_case computable detype detype_eqn tenv avoid env indsp st p k c bl =
     if synth_type & computable & bl <> [||] then
       Anonymous, None, None, None
     else
-      let p = option_app (detype tenv avoid env) p in
+      let p = option_app detype p in
       match p with
         | None -> Anonymous, None, None, None
         | Some p ->
             let decompose_lam k c =
-              let name_cons = function
-                  Anonymous -> fun l -> l | Name id -> fun l -> id::l in
               let rec lamdec_rec l avoid k c =
                 if k = 0 then l,c else match c with
                   | RLambda (_,x,t,c) -> 
@@ -241,7 +239,7 @@ let detype_case computable detype detype_eqn tenv avoid env indsp st p k c bl =
             n, aliastyp, Some typ, Some p
   in
   let constructs = Array.init (Array.length bl) (fun i -> (indsp,i+1)) in
-  let eqnv = array_map3 (detype_eqn tenv avoid env) constructs consnargsl bl in
+  let eqnv = array_map3 detype_eqn constructs consnargsl bl in
   let eqnl = Array.to_list eqnv in
   let tag =
     try 
@@ -256,7 +254,7 @@ let detype_case computable detype detype_eqn tenv avoid env indsp st p k c bl =
   if tag = RegularStyle then
     RCases (dummy_loc,(pred,ref newpred),[tomatch,ref (alias,aliastyp)],eqnl)
   else
-    let bl = Array.map (detype tenv avoid env) bl in
+    let bl = Array.map detype bl in
     if not !Options.v7 && tag = LetStyle && aliastyp = None then
       let rec decomp_lam_force n avoid l p =
 	if n = 0 then (List.rev l,p) else
@@ -340,8 +338,8 @@ let rec detype tenv avoid env t =
 	let comp = computable p (annot.ci_pp_info.ind_nargs) in
 	let ind = annot.ci_ind in
 	let st = annot.ci_pp_info.style in
-	detype_case comp detype detype_eqn tenv avoid env ind st (Some p)
-          annot.ci_pp_info.ind_nargs c bl
+	detype_case comp (detype tenv avoid env) (detype_eqn tenv avoid env)
+	  (snd tenv) avoid ind st (Some p) annot.ci_pp_info.ind_nargs c bl
     | Fix (nvn,recdef) -> detype_fix tenv avoid env nvn recdef
     | CoFix (n,recdef) -> detype_cofix tenv avoid env n recdef
 
@@ -437,11 +435,10 @@ and detype_eqn tenv avoid env constr construct_nargs branch =
 
 and detype_binder tenv bk avoid env na ty c =
   let na',avoid' =
-    if bk = BLetIn then concrete_let_name tenv avoid env na c
+    if bk = BLetIn then
+      concrete_let_name (fst tenv) avoid env na c
     else
-      match concrete_name tenv avoid env na c with
-	| (Some id,l') -> (Name id), l'
-	| (None,l')    -> Anonymous, l' in
+      concrete_name (fst tenv) avoid env na c in
   let r =  detype tenv avoid' (add_name na' env) c in
   match bk with
     | BProd -> RProd (dummy_loc, na',detype tenv [] env ty, r)
diff --git a/pretyping/detyping.mli b/pretyping/detyping.mli
index 5cf174875a..253e0f51c8 100644
--- a/pretyping/detyping.mli
+++ b/pretyping/detyping.mli
@@ -20,15 +20,14 @@ open Termops
 (* [detype env avoid nenv c] turns [c], typed in [env], into a rawconstr. *)
 (* De Bruijn indexes are turned to bound names, avoiding names in [avoid] *)
 
-val detype : env -> identifier list -> names_context -> constr -> rawconstr
+val detype : bool * env -> identifier list -> names_context -> constr -> 
+  rawconstr
 
 val detype_case : 
-  bool ->
-  (env -> identifier list -> names_context -> 'a -> rawconstr) ->
-  (env -> identifier list -> names_context -> constructor -> int -> 
-    'a -> Rawterm.loc * Names.identifier list * Rawterm.cases_pattern list *
-    Rawterm.rawconstr) ->
-    env -> identifier list -> names_context -> inductive -> case_style ->
+  bool -> ('a -> rawconstr) ->
+  (constructor -> int -> 'a -> loc * identifier list * cases_pattern list *
+    rawconstr) ->
+    env -> identifier list -> inductive -> case_style ->
       'a option -> int -> 'a -> 'a array -> rawconstr
 
 (* look for the index of a named var or a nondep var as it is renamed *)
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 145dc87202..a0fbb77241 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -759,7 +759,7 @@ let rec pretype tycon env isevars lvar = function
           let nconstr = Array.length mip.mind_consnames in
           let tyi = snd ind in
           if isrec && mis_is_recursive_subset [tyi] recargs then
-            Some (Detyping.detype env 
+            Some (Detyping.detype (false,env)
 	      (ids_of_context env) (names_of_rel_context env)
               (nf_evar (evars_of isevars) v))
 	  else
diff --git a/pretyping/termops.ml b/pretyping/termops.ml
index 6cf9b4e0db..c7786b2e1c 100644
--- a/pretyping/termops.ml
+++ b/pretyping/termops.ml
@@ -714,7 +714,7 @@ let occur_rel p env id =
   try lookup_name_of_rel p env = Name id
   with Not_found -> false (* Unbound indice : may happen in debug *)
 
-let occur_id env nenv id0 c =
+let occur_id nenv id0 c =
   let rec occur n c = match kind_of_term c with
     | Var id when  id=id0 -> raise Occur
     | Const kn when id_of_global (ConstRef kn) = id0 -> raise Occur
@@ -731,11 +731,11 @@ let occur_id env nenv id0 c =
   with Occur -> true
     | Not_found -> false (* Case when a global is not in the env *)
 
-let next_name_not_occuring env name l env_names t =
+let next_name_not_occuring is_goal_ccl name l env_names t =
   let rec next id =
-    if List.mem id l or occur_id env env_names id t or 
+    if List.mem id l or occur_id env_names id t or 
       (* To be consistent with intro mechanism *)
-      (is_global id & not (is_section_variable id))
+      (is_goal_ccl & is_global id & not (is_section_variable id))
     then next (lift_ident id)
     else id
   in 
@@ -826,16 +826,16 @@ let global_vars_set_of_decl env = function
         (global_vars_set env c)
 
 (* Remark: Anonymous var may be dependent in Evar's contexts *)
-let concrete_name env l env_names n c =
+let concrete_name is_goal_ccl l env_names n c =
   if n = Anonymous & noccurn 1 c then
-    (None,l)
+    (Anonymous,l)
   else
-    let fresh_id = next_name_not_occuring env n l env_names c in
-    let idopt = if noccurn 1 c then None else (Some fresh_id) in
+    let fresh_id = next_name_not_occuring is_goal_ccl n l env_names c in
+    let idopt = if noccurn 1 c then Anonymous else Name fresh_id in
     (idopt, fresh_id::l)
 
-let concrete_let_name env l env_names n c =
-  let fresh_id = next_name_not_occuring env n l env_names c in
+let concrete_let_name is_goal_ccl l env_names n c =
+  let fresh_id = next_name_not_occuring is_goal_ccl n l env_names c in
   (Name fresh_id, fresh_id::l)
 
 let rec rename_bound_var env l c =
diff --git a/pretyping/termops.mli b/pretyping/termops.mli
index 9031ec42de..0f970706a3 100644
--- a/pretyping/termops.mli
+++ b/pretyping/termops.mli
@@ -151,16 +151,15 @@ val add_vname : Idset.t -> name -> Idset.t
 (* sets of free identifiers *)
 type used_idents = identifier list
 val occur_rel : int -> name list -> identifier -> bool
-val occur_id : env -> name list -> identifier -> constr -> bool
+val occur_id : name list -> identifier -> constr -> bool
 
 val next_name_not_occuring :
-  env -> name -> identifier list -> name list -> constr -> identifier
+  bool -> name -> identifier list -> name list -> constr -> identifier
 val concrete_name :
-  env -> identifier list -> name list -> name ->
-  constr -> identifier option * identifier list
+  bool -> identifier list -> name list -> name -> constr -> 
+    name * identifier list
 val concrete_let_name :
-  env -> identifier list -> name list ->
-  name -> constr -> name * identifier list
+  bool -> identifier list -> name list -> name -> constr -> name * identifier list
 val rename_bound_var : env -> identifier list -> types -> types
 
 (* other signature iterators *)