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

9 files changed, 58 insertions, 65 deletions

diff --git a/contrib/correctness/pcic.ml b/contrib/correctness/pcic.ml
index bef1e2a23c..db2617da33 100644
--- a/contrib/correctness/pcic.ml
+++ b/contrib/correctness/pcic.ml
@@ -137,7 +137,7 @@ let tuple_ref dep n =
 
 let trad_binder avoid nenv id = function
   | CC_untyped_binder -> RHole (dummy_loc,BinderType (Name id))
-  | CC_typed_binder ty -> Detyping.detype (Global.env()) avoid nenv ty
+  | CC_typed_binder ty -> Detyping.detype (false,Global.env()) avoid nenv ty
 
 let rec push_vars avoid nenv = function
   | [] -> ([],avoid,nenv)
@@ -209,22 +209,22 @@ let rawconstr_of_prog p =
       	let n = List.length l in
       	let cl = List.map (trad avoid nenv) l in
       	let tuple = tuple_ref dep n in
-	let tyl = List.map (Detyping.detype (Global.env()) avoid nenv) tyl in
+	let tyl = List.map (Detyping.detype (false,Global.env()) avoid nenv) tyl in
       	let args = tyl @ cl in
 	RApp (dummy_loc, RRef (dummy_loc, tuple), args)
 
     | CC_case (ty,b,el) ->
 	let c = trad avoid nenv b in
 	let cl = List.map (trad avoid nenv) el in
-	let ty = Detyping.detype (Global.env()) avoid nenv ty in
+	let ty = Detyping.detype (false,Global.env()) avoid nenv ty in
 	ROrderedCase (dummy_loc, RegularStyle, Some ty, c, Array.of_list cl, ref None)
 
     | CC_expr c -> 
-	Detyping.detype (Global.env()) avoid nenv c
+	Detyping.detype (false,Global.env()) avoid nenv c
 
     | CC_hole c -> 
 	RCast (dummy_loc, RHole (dummy_loc, QuestionMark),
-               Detyping.detype (Global.env()) avoid nenv c)
+               Detyping.detype (false,Global.env()) avoid nenv c)
 
   in
   trad [] empty_names_context p
diff --git a/contrib/first-order/instances.ml b/contrib/first-order/instances.ml
index 1dc72eecb8..423df2f3c7 100644
--- a/contrib/first-order/instances.ml
+++ b/contrib/first-order/instances.ml
@@ -121,7 +121,7 @@ let mk_open_instance id gl m t=
       let nid=(fresh_id avoid var_id gl) in
 	(Name nid,None,dummy_constr)::(aux (n-1) (nid::avoid)) in
   let nt=it_mkLambda_or_LetIn revt (aux m []) in
-  let rawt=Detyping.detype env [] [] nt in
+  let rawt=Detyping.detype (false,env) [] [] nt in
   let rec raux n t=
     if n=0 then t else 
       match t with
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index b34ae524f2..2eae4a51b9 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -738,7 +738,7 @@ let extern_constr_gen at_top scopt env t =
   let vars = vars_of_env env in
   let avoid = if at_top then ids_of_context env else [] in
   extern (not at_top) (scopt,Symbols.current_scopes()) vars
-    (Detyping.detype env avoid (names_of_rel_context env) t)
+    (Detyping.detype (at_top,env) avoid (names_of_rel_context env) t)
 
 let extern_constr_in_scope at_top scope env t =
   extern_constr_gen at_top (Some scope) env t
@@ -782,13 +782,11 @@ let rec raw_of_pat tenv env = function
   | PCase ((Some ind,cs),typopt,tm,bv) ->
       let avoid = List.fold_right (name_fold (fun x l -> x::l)) env [] in
       let k = (snd (lookup_mind_specif (Global.env()) ind)).Declarations.mind_nrealargs in
-      Detyping.detype_case false
-	(fun tenv _ -> raw_of_pat tenv)
-	(fun tenv _ -> raw_of_eqn tenv)
-	tenv avoid env ind cs typopt k tm bv
+      Detyping.detype_case false (raw_of_pat tenv env)(raw_of_eqn tenv env)
+	tenv avoid ind cs typopt k tm bv
   | PCase _ -> error "Unsupported case-analysis while printing pattern"
-  | PFix f -> Detyping.detype tenv [] env (mkFix f)
-  | PCoFix c -> Detyping.detype tenv [] env (mkCoFix c)
+  | PFix f -> Detyping.detype (false,tenv) [] env (mkFix f)
+  | PCoFix c -> Detyping.detype (false,tenv) [] env (mkCoFix c)
   | PSort s -> RSort (loc,s)
 
 and raw_of_eqn tenv env constr construct_nargs branch =
diff --git a/parsing/termast.ml b/parsing/termast.ml
index da683e5fa8..3174898c42 100644
--- a/parsing/termast.ml
+++ b/parsing/termast.ml
@@ -337,7 +337,7 @@ let ast_of_constr at_top env t =
     else Reductionops.local_strong strip_outer_cast t in
   let avoid = if at_top then ids_of_context env else [] in
   ast_of_raw 
-    (Detyping.detype env avoid (names_of_rel_context env) t')
+    (Detyping.detype (at_top,env) avoid (names_of_rel_context env) t')
 
 let ast_of_constant env sp =
   let a = ast_of_constant_ref sp in
@@ -432,8 +432,8 @@ let rec ast_of_pattern tenv env = function
 
   | PMeta (Some n) -> ope("META",[ast_of_ident n])
   | PMeta None -> ope("ISEVAR",[])
-  | PFix f -> ast_of_raw (Detyping.detype tenv [] env (mkFix f))
-  | PCoFix c -> ast_of_raw (Detyping.detype tenv [] env (mkCoFix c))
+  | PFix f -> ast_of_raw (Detyping.detype (false,tenv) [] env (mkFix f))
+  | PCoFix c -> ast_of_raw (Detyping.detype (false,tenv) [] env (mkCoFix c))
 	
 and ast_of_patopt tenv env = function
   | None -> (string "SYNTH")
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 *)