diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-11-30 00:33:08 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-02-14 17:30:44 +0100 |
| commit | 1683b718f85134fdb0d49535e489344e1a7d56f5 (patch) | |
| tree | 5750652739a4c80c793573b29bc8f73194ed1a7f /engine/evarutil.ml | |
| parent | 27fbf069ccd846383bcfb35ba1ea5bd1d95090a0 (diff) | |
Making Evd independent from Namegen.
Diffstat (limited to 'engine/evarutil.ml')
| -rw-r--r-- | engine/evarutil.ml | 10 |
1 files changed, 9 insertions, 1 deletions
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 |