From 1683b718f85134fdb0d49535e489344e1a7d56f5 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Wed, 30 Nov 2016 00:33:08 +0100 Subject: Making Evd independent from Namegen. --- engine/evarutil.ml | 10 +++++++++- 1 file changed, 9 insertions(+), 1 deletion(-) (limited to 'engine/evarutil.ml') diff --git a/engine/evarutil.ml b/engine/evarutil.ml index 0582e34be..e94fd72f1 100644 --- a/engine/evarutil.ml +++ b/engine/evarutil.ml @@ -418,6 +418,14 @@ let new_pure_evar sign evd ?(src=default_source) ?(filter = Filter.identity) ?ca let candidates = Option.map (fun l -> List.map EConstr.Unsafe.to_constr l) candidates in let default_naming = Misctypes.IntroAnonymous in let naming = Option.default default_naming naming in + let name = match naming with + | Misctypes.IntroAnonymous -> None + | Misctypes.IntroIdentifier id -> Some id + | Misctypes.IntroFresh id -> + let has_name id = try let _ = Evd.evar_key id evd in true with Not_found -> false in + let id = Namegen.next_ident_away_from id has_name in + Some id + in let evi = { evar_hyps = sign; evar_concl = typ; @@ -427,7 +435,7 @@ let new_pure_evar sign evd ?(src=default_source) ?(filter = Filter.identity) ?ca evar_candidates = candidates; evar_extra = store; } in - let (evd, newevk) = Evd.new_evar evd ~naming evi in + let (evd, newevk) = Evd.new_evar evd ?name evi in let evd = if principal then Evd.declare_principal_goal newevk evd else Evd.declare_future_goal newevk evd -- cgit v1.2.3