diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-11-09 18:05:13 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-11-09 18:05:13 +0000 |
| commit | 1a4a7fa6dbd7c43c5d6c99297d1b6c5c497c0589 (patch) | |
| tree | fc18af5b3330e830a8e979bc551db46b25bda05d /toplevel | |
| parent | cb2f5d06481f9021f600eaefbdc6b33118bd346d (diff) | |
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
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/classes.ml | 2 | ||||
| -rw-r--r-- | toplevel/himsg.ml | 1 | ||||
| -rw-r--r-- | toplevel/lemmas.ml | 3 | ||||
| -rw-r--r-- | toplevel/record.ml | 4 | ||||
| -rw-r--r-- | toplevel/vernacentries.ml | 2 |
5 files changed, 7 insertions, 5 deletions
diff --git a/toplevel/classes.ml b/toplevel/classes.ml index 063fe7a10..8412a39f3 100644 --- a/toplevel/classes.ml +++ b/toplevel/classes.ml @@ -170,7 +170,7 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(generalize=true) id | Anonymous -> let i = Nameops.add_suffix (id_of_class k) "_instance_0" in - Termops.next_global_ident_away false i (Termops.ids_of_context env) + Namegen.next_global_ident_away i (Termops.ids_of_context env) in let env' = push_rel_context ctx' env in evars := Evarutil.nf_evar_defs !evars; diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml index 6b8c45fec..c769e8930 100644 --- a/toplevel/himsg.ml +++ b/toplevel/himsg.ml @@ -13,6 +13,7 @@ open Util open Flags open Names open Nameops +open Namegen open Term open Termops open Inductive diff --git a/toplevel/lemmas.ml b/toplevel/lemmas.ml index 7ea001259..d9a26b427 100644 --- a/toplevel/lemmas.ml +++ b/toplevel/lemmas.ml @@ -26,6 +26,7 @@ open Decl_kinds open Declare open Pretyping open Termops +open Namegen open Evd open Evarutil open Reductionops @@ -175,7 +176,7 @@ let compute_proof_name = function id | None -> let rec next avoid id = - let id = next_global_ident_away false id avoid in + let id = next_global_ident_away id avoid in if Nametab.exists_cci (Lib.make_path id) then next (id::avoid) id else id in diff --git a/toplevel/record.ml b/toplevel/record.ml index 1a3e5102e..5ed989438 100644 --- a/toplevel/record.ml +++ b/toplevel/record.ml @@ -162,7 +162,7 @@ let declare_projections indsp ?(kind=StructureComponent) ?name coers fieldimpls let r = mkInd indsp in let rp = applist (r, extended_rel_list 0 paramdecls) in let paramargs = extended_rel_list 1 paramdecls in (*def in [[params;x:rp]]*) - let x = match name with Some n -> Name n | None -> Termops.named_hd (Global.env()) r Anonymous in + let x = match name with Some n -> Name n | None -> Namegen.named_hd (Global.env()) r Anonymous in let fields = instantiate_possibly_recursive_type indsp paramdecls fields in let lifted_fields = lift_rel_context 1 fields in let (_,kinds,sp_projs,_) = @@ -332,7 +332,7 @@ let declare_class finite def infer id idbuild paramimpls params arity fieldimpls if infer then Evd.fold (fun ev evi _ -> Recordops.declare_method (ConstRef cst) ev sign) sign (); cref, [proj_name, Some proj_cst] | _ -> - let idarg = Nameops.next_ident_away (snd id) (ids_of_context (Global.env())) in + let idarg = Namegen.next_ident_away (snd id) (ids_of_context (Global.env())) in let ind = declare_structure BiFinite infer (snd id) idbuild paramimpls params (Option.cata (fun x -> x) (new_Type ()) arity) fieldimpls fields ~kind:Method ~name:idarg false (List.map (fun _ -> false) fields) sign diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 3d7751d97..e3aa41354 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -153,7 +153,7 @@ let make_cases s = let rec rename avoid = function | [] -> [] | (n,_)::l -> - let n' = Termops.next_global_ident_away true (id_of_name n) avoid in + let n' = Namegen.next_ident_away_in_goal (id_of_name n) avoid in string_of_id n' :: rename (n'::avoid) l in let al' = rename [] (List.rev al) in (string_of_id n :: al') :: l) |