A bit of cleaning around name generation + creation of dedicated file namegen.ml

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

9 files changed, 68 insertions, 67 deletions

diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 3d789b92ed..e8ec962b44 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -2,6 +2,7 @@ open Printer
 open Util
 open Term
 open Termops
+open Namegen
 open Names
 open Declarations
 open Pp
@@ -1358,7 +1359,7 @@ let prove_with_tcc tcc_lemma_constr eqs : tactic =
     | None -> anomaly "No tcc proof !!"
     | Some lemma ->
 	fun gls ->
-(* 	  let hid = next_global_ident_away true h_id (pf_ids_of_hyps gls) in *)
+(* 	  let hid = next_ident_away_in_goal h_id (pf_ids_of_hyps gls) in *)
 (* 	  let ids = hid::pf_ids_of_hyps gls in  *)
 	  tclTHENSEQ
 	    [
@@ -1581,7 +1582,7 @@ let prove_principle_for_gen
   let start_tac gls =
     let hyps = pf_ids_of_hyps gls in
       let hid =
-	next_global_ident_away true
+	next_ident_away_in_goal
 	  (id_of_string "prov")
 	  hyps
       in
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index ff4d1e972f..b756492b51 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -2,6 +2,7 @@ open Printer
 open Util
 open Term
 open Termops
+open Namegen
 open Names
 open Declarations
 open Pp
@@ -67,7 +68,7 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type =
     match predicates with
     | [] -> []
     |(Name x,v,t)::predicates ->
-       let id =  Nameops.next_ident_away x avoid in
+       let id =  Namegen.next_ident_away x avoid in
        Hashtbl.add tbl id x;
        (Name id,v,t)::(change_predicates_names (id::avoid) predicates)
     | (Anonymous,_,_)::_ -> anomaly "Anonymous property binder "
@@ -330,7 +331,7 @@ let build_functional_principle interactive_proof old_princ_type sorts funs i pro
   (*    Pp.msgnl (str "computing principle type := " ++ System.fmt_time_difference time1 time2); *)
      observe (str "new_principle_type : " ++ pr_lconstr new_principle_type);
   let new_princ_name =
-    next_global_ident_away true (id_of_string "___________princ_________") []
+    next_ident_away_in_goal (id_of_string "___________princ_________") []
   in
   begin
     Lemmas.start_proof
diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4
index 0e51eb7e1b..64f9403a1c 100644
--- a/plugins/funind/g_indfun.ml4
+++ b/plugins/funind/g_indfun.ml4
@@ -383,7 +383,7 @@ let rec poseq_list_ids_rec lcstr gl =
 	      let _ = prconstr c in
 	      let _ = prstr "\n" in
 	      let typ = Tacmach.pf_type_of gl c in
-	      let cname = Termops.id_of_name_using_hdchar (Global.env()) typ Anonymous in
+	      let cname = Namegen.id_of_name_using_hdchar (Global.env()) typ Anonymous in
 	      let x = Tactics.fresh_id [] cname gl in
 	      let _ = list_constr_largs:=mkVar x :: !list_constr_largs in
 	      let _ = prstr " list_constr_largs = " in
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index 53359e31d7..fb1204c1f6 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -15,7 +15,7 @@ let msgnl m =
 let invalid_argument s = raise (Invalid_argument s)
 
 
-let fresh_id avoid s = Termops.next_global_ident_away true (id_of_string s) avoid
+let fresh_id avoid s = Namegen.next_ident_away_in_goal (id_of_string s) avoid
 
 let fresh_name avoid s = Name (fresh_id avoid s)
 
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index ca93056ad1..ca608ec0ba 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -117,14 +117,12 @@ let generate_type g_to_f f graph i =
   in
   (*i We need to name the vars [res] and [fv] i*)
   let res_id =
-    Termops.next_global_ident_away
-      true
+    Namegen.next_ident_away_in_goal
       (id_of_string "res")
       (map_succeed (function (Name id,_,_) -> id | (Anonymous,_,_) -> failwith "") fun_ctxt)
   in
   let fv_id =
-    Termops.next_global_ident_away
-      true
+    Namegen.next_ident_away_in_goal
       (id_of_string "fv")
       (res_id::(map_succeed (function (Name id,_,_) -> id | (Anonymous,_,_) -> failwith "Anonymous!") fun_ctxt))
   in
@@ -209,7 +207,7 @@ let rec generate_fresh_id x avoid i =
   if i == 0
   then []
   else
-    let id = Termops.next_global_ident_away true x avoid in
+    let id = Namegen.next_ident_away_in_goal x avoid in
     id::(generate_fresh_id x (id::avoid) (pred i))
 
 
@@ -271,7 +269,7 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem
        environement and due to the bug #1174, we will need to pose the principle
        using a name
     *)
-    let principle_id = Termops.next_global_ident_away true (id_of_string "princ") ids in
+    let principle_id = Namegen.next_ident_away_in_goal (id_of_string "princ") ids in
     let ids = principle_id :: ids in
     (* We get the branches of the principle *)
     let branches = List.rev princ_infos.branches in
@@ -425,7 +423,7 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem
       let params_bindings,avoid =
 	List.fold_left2
 	  (fun (bindings,avoid) (x,_,_) p ->
-	     let id = Nameops.next_ident_away (Nameops.out_name x) avoid in
+	     let id = Namegen.next_ident_away (Nameops.out_name x) avoid in
 	     (dummy_loc,Rawterm.NamedHyp id,inj_open p)::bindings,id::avoid
 	  )
 	  ([],pf_ids_of_hyps g)
@@ -435,7 +433,7 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem
       let lemmas_bindings =
 	List.rev (fst  (List.fold_left2
 	  (fun (bindings,avoid) (x,_,_) p ->
-	     let id = Nameops.next_ident_away (Nameops.out_name x) avoid in
+	     let id = Namegen.next_ident_away (Nameops.out_name x) avoid in
 	     (dummy_loc,Rawterm.NamedHyp id,inj_open (nf_zeta p))::bindings,id::avoid)
 	  ([],avoid)
 	  princ_infos.predicates
diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml
index 6dc36decf3..04e36d945d 100644
--- a/plugins/funind/merge.ml
+++ b/plugins/funind/merge.ml
@@ -77,7 +77,7 @@ let ident_global_exist id =
     global env) with base [id]. *)
 let next_ident_fresh (id:identifier) =
     let res = ref id in
-    while ident_global_exist !res do res := Nameops.lift_ident !res done;
+    while ident_global_exist !res do res := Nameops.lift_subscript !res done;
     !res
 
 
diff --git a/plugins/funind/rawterm_to_relation.ml b/plugins/funind/rawterm_to_relation.ml
index 607734f222..752e546c89 100644
--- a/plugins/funind/rawterm_to_relation.ml
+++ b/plugins/funind/rawterm_to_relation.ml
@@ -138,7 +138,7 @@ let apply_args ctxt body args =
   let next_name_away (na:name) (mapping: identifier Idmap.t) (avoid: identifier list) =
     match na with
        | Name id when List.mem id avoid ->
-	   let new_id = Nameops.next_ident_away id avoid in
+	   let new_id = Namegen.next_ident_away id avoid in
 	   Name new_id,Idmap.add id new_id mapping,new_id::avoid
        | _ -> na,mapping,avoid
   in
@@ -168,7 +168,7 @@ let apply_args ctxt body args =
 	    if need_convert_id avoid id
 	    then
 	      let new_avoid =  id::avoid in
-	      let new_id = Nameops.next_ident_away id new_avoid in
+	      let new_id = Namegen.next_ident_away id new_avoid in
 	      let new_avoid' = new_id :: new_avoid in
 	      let mapping = Idmap.add id new_id Idmap.empty in
 	      let new_ctxt' = change_vars_in_binder mapping ctxt' in
@@ -550,7 +550,7 @@ let rec build_entry_lc env funnames avoid rt  : rawconstr build_entry_return =
 		  match n with
 		    | Name id when List.exists (is_free_in id) args ->
 			(* need to alpha-convert the name *)
-			let new_id = Nameops.next_ident_away id avoid in
+			let new_id = Namegen.next_ident_away id avoid in
 			let new_avoid = id:: avoid in
 			let new_b =
 			  replace_var_by_term
diff --git a/plugins/funind/rawtermops.ml b/plugins/funind/rawtermops.ml
index 502960a144..e31f1452d9 100644
--- a/plugins/funind/rawtermops.ml
+++ b/plugins/funind/rawtermops.ml
@@ -202,7 +202,7 @@ let rec alpha_pat excluded pat =
     | PatVar(loc,Name id) ->
 	if List.mem id excluded
 	then
-	  let new_id = Nameops.next_ident_away id excluded in
+	  let new_id = Namegen.next_ident_away id excluded in
 	  PatVar(loc,Name new_id),(new_id::excluded),
 	(Idmap.add id new_id Idmap.empty)
 	else pat,excluded,Idmap.empty
@@ -210,7 +210,7 @@ let rec alpha_pat excluded pat =
 	let new_na,new_excluded,map =
 	  match na with
 	    | Name id when List.mem id excluded ->
-		let new_id = Nameops.next_ident_away id excluded in
+		let new_id = Namegen.next_ident_away id excluded in
 		Name new_id,new_id::excluded, Idmap.add id new_id Idmap.empty
 	    | _ -> na,excluded,Idmap.empty
 	in
@@ -264,7 +264,7 @@ let rec alpha_rt excluded rt =
     match rt with
       | RRef _ | RVar _ | REvar _ | RPatVar _ -> rt
       | RLambda(loc,Anonymous,k,t,b) ->
-	  let new_id = Nameops.next_ident_away (id_of_string "_x") excluded in
+	  let new_id = Namegen.next_ident_away (id_of_string "_x") excluded in
 	  let new_excluded = new_id :: excluded in
 	  let new_t = alpha_rt new_excluded t in
 	  let new_b = alpha_rt new_excluded b in
@@ -278,7 +278,7 @@ let rec alpha_rt excluded rt =
 	let new_b = alpha_rt excluded b in
 	RLetIn(loc,Anonymous,new_t,new_b)
     | RLambda(loc,Name id,k,t,b) ->
-	let new_id = Nameops.next_ident_away id excluded in
+	let new_id = Namegen.next_ident_away id excluded in
 	let t,b =
 	  if new_id = id
 	  then t,b
@@ -291,7 +291,7 @@ let rec alpha_rt excluded rt =
 	let new_b = alpha_rt new_excluded b in
 	RLambda(loc,Name new_id,k,new_t,new_b)
     | RProd(loc,Name id,k,t,b) ->
-	let new_id = Nameops.next_ident_away id excluded in
+	let new_id = Namegen.next_ident_away id excluded in
 	let new_excluded = new_id::excluded in
 	let t,b =
 	  if new_id = id
@@ -304,7 +304,7 @@ let rec alpha_rt excluded rt =
 	let new_b = alpha_rt new_excluded b in
 	RProd(loc,Name new_id,k,new_t,new_b)
     | RLetIn(loc,Name id,t,b) ->
-	let new_id = Nameops.next_ident_away id excluded in
+	let new_id = Namegen.next_ident_away id excluded in
 	let t,b =
 	  if new_id = id
 	  then t,b
@@ -325,7 +325,7 @@ let rec alpha_rt excluded rt =
 	       match na with
 		 | Anonymous -> (na::nal,excluded,mapping)
 		 | Name id ->
-		     let new_id = Nameops.next_ident_away id excluded in
+		     let new_id = Namegen.next_ident_away id excluded in
 		     if new_id = id
 		     then
 		       na::nal,id::excluded,mapping
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index d64b9728b4..469f87f15b 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -12,6 +12,7 @@
 
 open Term
 open Termops
+open Namegen
 open Environ
 open Declarations
 open Entries
@@ -50,7 +51,7 @@ open Genarg
 
 
 let compute_renamed_type gls c =
-  rename_bound_var (pf_env gls) [] (pf_type_of gls c)
+  rename_bound_vars_as_displayed (pf_env gls) [] (pf_type_of gls c)
 
 let qed () = Lemmas.save_named true
 let defined () = Lemmas.save_named false
@@ -58,7 +59,7 @@ let defined () = Lemmas.save_named false
 let pf_get_new_ids idl g =
   let ids = pf_ids_of_hyps g in
   List.fold_right
-    (fun id acc -> next_global_ident_away false id (acc@ids)::acc)
+    (fun id acc -> next_global_ident_away id (acc@ids)::acc)
     idl
     []
 
@@ -515,11 +516,11 @@ let rec introduce_all_equalities func eqs values specs bound le_proofs
       fun g ->
 	let ids = pf_ids_of_hyps g in
 	let s_max = mkApp(delayed_force coq_S, [|bound|]) in
-	let k = next_global_ident_away true k_id ids in
+	let k = next_ident_away_in_goal k_id ids in
         let ids = k::ids in
-	let h' = next_global_ident_away true (h'_id) ids in
+	let h' = next_ident_away_in_goal (h'_id) ids in
         let ids = h'::ids in
-	let def = next_global_ident_away true def_id ids in
+	let def = next_ident_away_in_goal def_id ids in
 	tclTHENLIST
 	  [observe_tac "introduce_all_equalities_final split" (split (ImplicitBindings [s_max]));
 	   observe_tac "introduce_all_equalities_final intro k" (h_intro  k);
@@ -543,15 +544,15 @@ let rec introduce_all_equalities func eqs values specs bound le_proofs
   | spec1::specs ->
       fun g ->
 	let ids = ids_of_named_context (pf_hyps g) in
-	let p = next_global_ident_away true p_id ids in
+	let p = next_ident_away_in_goal p_id ids in
         let ids = p::ids in
-	let pmax = next_global_ident_away true pmax_id ids in
+	let pmax = next_ident_away_in_goal pmax_id ids in
         let ids = pmax::ids in
-	let hle1 = next_global_ident_away true hle_id ids in
+	let hle1 = next_ident_away_in_goal hle_id ids in
         let ids = hle1::ids in
-	let hle2 = next_global_ident_away true  hle_id ids in
+	let hle2 = next_ident_away_in_goal  hle_id ids in
 	let ids = hle2::ids in
-	let heq = next_global_ident_away true heq_id ids in
+	let heq = next_ident_away_in_goal heq_id ids in
 	tclTHENLIST
 	  [simplest_elim (mkVar spec1);
 	   list_rewrite true eqs;
@@ -589,9 +590,9 @@ let rec introduce_all_values concl_tac is_mes acc_inv func context_fn
   | arg::args ->
       (fun g ->
 	let ids = ids_of_named_context (pf_hyps g) in
-	let rec_res = next_global_ident_away true rec_res_id ids in
+	let rec_res = next_ident_away_in_goal rec_res_id ids in
         let ids = rec_res::ids in
-	let hspec = next_global_ident_away true hspec_id ids in
+	let hspec = next_ident_away_in_goal hspec_id ids in
 	let tac =
 	  observe_tac "introduce_all_values" (
 	    introduce_all_values concl_tac is_mes acc_inv func context_fn eqs
@@ -722,13 +723,13 @@ let termination_proof_header is_mes input_type ids args_id relation
       in
       let relation = substl pre_rec_args relation in
       let input_type = substl pre_rec_args input_type in
-      let wf_thm = next_global_ident_away true (id_of_string ("wf_R")) ids in
+      let wf_thm = next_ident_away_in_goal (id_of_string ("wf_R")) ids in
       let wf_rec_arg =
-	next_global_ident_away true
+	next_ident_away_in_goal
 	  (id_of_string ("Acc_"^(string_of_id rec_arg_id)))
 	  (wf_thm::ids)
       in
-      let hrec = next_global_ident_away true hrec_id
+      let hrec = next_ident_away_in_goal hrec_id
 	(wf_rec_arg::wf_thm::ids) in
       let acc_inv =
 	  lazy (
@@ -806,7 +807,7 @@ let whole_start (concl_tac:tactic) nb_args is_mes func input_type relation rec_a
       let (f_name, _, body1) = destLambda func_body in
       let f_id =
 	match f_name with
-	  | Name f_id -> next_global_ident_away true f_id ids
+	  | Name f_id -> next_ident_away_in_goal f_id ids
 	  | Anonymous -> anomaly "Anonymous function"
       in
       let n_names_types,_ = decompose_lam_n nb_args body1 in
@@ -815,7 +816,7 @@ let whole_start (concl_tac:tactic) nb_args is_mes func input_type relation rec_a
 	  (fun (n_ids,ids) (n_name,_) ->
 	     match n_name with
 	       | Name id ->
-		   let n_id = next_global_ident_away true id ids in
+		   let n_id = next_ident_away_in_goal id ids in
 		   n_id::n_ids,n_id::ids
 	       | _ -> anomaly "anonymous argument"
 	  )
@@ -906,7 +907,7 @@ let build_new_goal_type () =
     (*
 let prove_with_tcc lemma _ : tactic =
   fun gls ->
-    let hid = next_global_ident_away true h_id (pf_ids_of_hyps gls) in
+    let hid = next_ident_away_in_goal h_id (pf_ids_of_hyps gls) in
     tclTHENSEQ
       [
 	h_generalize [lemma];
@@ -930,7 +931,7 @@ let open_new_goal (build_proof:tactic -> tactic -> unit) using_lemmas ref_ goal_
   in
   let sign = Global.named_context () in
   let sign = clear_proofs sign in
-  let na = next_global_ident_away false name [] in
+  let na = next_global_ident_away name [] in
   if occur_existential gls_type then
     Util.error "\"abstract\" cannot handle existentials";
   let hook _ _ =
@@ -951,7 +952,7 @@ let open_new_goal (build_proof:tactic -> tactic -> unit) using_lemmas ref_ goal_
     Flags.silently Vernacentries.interp (Vernacexpr.VernacAbort None);
     build_proof
       (  fun gls ->
-	   let hid = next_global_ident_away true h_id (pf_ids_of_hyps gls) in
+	   let hid = next_ident_away_in_goal h_id (pf_ids_of_hyps gls) in
 	   tclTHENSEQ
 	     [
 	       h_generalize [lemma];
@@ -1075,7 +1076,7 @@ let (value_f:constr list -> global_reference -> constr) =
       (
 	List.fold_left
 	  (fun x_id_l _ ->
-	     let x_id = next_global_ident_away true x_id x_id_l in
+	     let x_id = next_ident_away_in_goal x_id x_id_l in
 	     x_id::x_id_l
 	  )
 	  []
@@ -1122,7 +1123,7 @@ let (declare_f : identifier -> logical_kind -> constr list -> global_reference -
 
 let rec n_x_id ids n =
   if n = 0 then []
-  else let x = next_global_ident_away true x_id ids in
+  else let x = next_ident_away_in_goal x_id ids in
           x::n_x_id (x::ids) (n-1);;
 
 let start_equation (f:global_reference) (term_f:global_reference)
@@ -1141,12 +1142,12 @@ let start_equation (f:global_reference) (term_f:global_reference)
 
 let base_leaf_eq func eqs f_id g =
   let ids = pf_ids_of_hyps g in
-  let k = next_global_ident_away true k_id ids in
-  let p = next_global_ident_away true p_id (k::ids) in
-  let v = next_global_ident_away true v_id (p::k::ids) in
-  let heq = next_global_ident_away true heq_id (v::p::k::ids) in
-  let heq1 = next_global_ident_away true heq_id (heq::v::p::k::ids) in
-  let hex = next_global_ident_away true hex_id (heq1::heq::v::p::k::ids) in
+  let k = next_ident_away_in_goal k_id ids in
+  let p = next_ident_away_in_goal p_id (k::ids) in
+  let v = next_ident_away_in_goal v_id (p::k::ids) in
+  let heq = next_ident_away_in_goal heq_id (v::p::k::ids) in
+  let heq1 = next_ident_away_in_goal heq_id (heq::v::p::k::ids) in
+  let hex = next_ident_away_in_goal hex_id (heq1::heq::v::p::k::ids) in
     tclTHENLIST [
       h_intros [v; hex];
       simplest_elim (mkVar hex);
@@ -1168,7 +1169,7 @@ let rec introduce_all_values_eq cont_tac functional termine
     f p heq1 pmax bounds le_proofs eqs ids =
   function
       [] ->
-       let heq2 = next_global_ident_away true heq_id ids in
+       let heq2 = next_ident_away_in_goal heq_id ids in
 	tclTHENLIST
 	  [pose_proof (Name heq2)
              (mkApp(mkVar heq1, [|f_S(f_S(mkVar pmax))|]));
@@ -1193,21 +1194,21 @@ let rec introduce_all_values_eq cont_tac functional termine
 	      tclTHENLIST[apply (delayed_force le_lt_SS);
 			compute_le_proofs le_proofs]]]
     | arg::args ->
-	let v' = next_global_ident_away true v_id ids in
+	let v' = next_ident_away_in_goal v_id ids in
         let ids = v'::ids in
-	let hex' = next_global_ident_away true hex_id ids in
+	let hex' = next_ident_away_in_goal hex_id ids in
         let ids = hex'::ids in
-	let p' = next_global_ident_away true p_id ids in
+	let p' = next_ident_away_in_goal p_id ids in
         let ids = p'::ids in
-	let new_pmax = next_global_ident_away true pmax_id ids in
+	let new_pmax = next_ident_away_in_goal pmax_id ids in
         let ids = pmax::ids in
-	let hle1 = next_global_ident_away true hle_id ids in
+	let hle1 = next_ident_away_in_goal hle_id ids in
         let ids = hle1::ids in
-	let hle2 = next_global_ident_away true hle_id ids in
+	let hle2 = next_ident_away_in_goal hle_id ids in
         let ids = hle2::ids in
-	let heq = next_global_ident_away true heq_id ids in
+	let heq = next_ident_away_in_goal heq_id ids in
         let ids = heq::ids in
-	let heq2 = next_global_ident_away true heq_id ids in
+	let heq2 = next_ident_away_in_goal heq_id ids in
         let ids = heq2::ids in
 	tclTHENLIST
 	  [mkCaseEq(mkApp(termine, Array.of_list arg));
@@ -1253,15 +1254,15 @@ let rec introduce_all_values_eq cont_tac functional termine
 
 
 let rec_leaf_eq termine f ids functional eqs expr fn args =
-  let p = next_global_ident_away true p_id ids in
+  let p = next_ident_away_in_goal p_id ids in
   let ids = p::ids in
-  let v = next_global_ident_away true v_id ids in
+  let v = next_ident_away_in_goal v_id ids in
   let ids = v::ids in
-  let hex = next_global_ident_away true hex_id ids in
+  let hex = next_ident_away_in_goal hex_id ids in
   let ids = hex::ids in
-  let heq1 = next_global_ident_away true heq_id ids in
+  let heq1 = next_ident_away_in_goal heq_id ids in
   let ids = heq1::ids in
-  let hle1 = next_global_ident_away true hle_id ids in
+  let hle1 = next_ident_away_in_goal hle_id ids in
   let ids = hle1::ids in
     tclTHENLIST
       [observe_tac "intros v hex" (h_intros [v;hex]);