diff options
| author | Pierre-Marie Pédrot | 2020-07-04 18:28:33 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-08-06 12:33:58 +0200 |
| commit | 29cc320bc3d54b9b4b8d78240db50cc8a878b033 (patch) | |
| tree | 079aaddfe31d534b5ea43f10e4c4f00a5e2808d4 /engine/evarutil.ml | |
| parent | 51ecccef0308eceec1ddd9776a03fd993b3ea71a (diff) | |
Store the default evar instance inside the evar info.
Diffstat (limited to 'engine/evarutil.ml')
| -rw-r--r-- | engine/evarutil.ml | 16 |
1 files changed, 12 insertions, 4 deletions
diff --git a/engine/evarutil.ml b/engine/evarutil.ml index b4b2032dd2..c3f189cdf0 100644 --- a/engine/evarutil.ml +++ b/engine/evarutil.ml @@ -409,8 +409,9 @@ let push_rel_context_to_named_context ?hypnaming env sigma typ = let default_source = Loc.tag @@ Evar_kinds.InternalHole -let new_pure_evar ?(src=default_source) ?(filter = Filter.identity) ?(abstract_arguments = Abstraction.identity) - ?candidates ?(naming = IntroAnonymous) ?typeclass_candidate ?(principal=false) sign evd typ = +let new_pure_evar ?(src=default_source) ?(filter = Filter.identity) ?identity + ?(abstract_arguments = Abstraction.identity) ?candidates + ?(naming = IntroAnonymous) ?typeclass_candidate ?(principal=false) sign evd typ = let name = match naming with | IntroAnonymous -> None | IntroIdentifier id -> Some id @@ -419,6 +420,10 @@ let new_pure_evar ?(src=default_source) ?(filter = Filter.identity) ?(abstract_a let id = Namegen.next_ident_away_from id has_name in Some id in + let identity = match identity with + | None -> Identity.none () + | Some inst -> Identity.make inst + in let evi = { evar_hyps = sign; evar_concl = typ; @@ -426,7 +431,9 @@ let new_pure_evar ?(src=default_source) ?(filter = Filter.identity) ?(abstract_a evar_filter = filter; evar_abstract_arguments = abstract_arguments; evar_source = src; - evar_candidates = candidates } + evar_candidates = candidates; + evar_identity = identity; + } in let typeclass_candidate = if principal then Some false else typeclass_candidate in let (evd, newevk) = Evd.new_evar evd ?name ?typeclass_candidate evi in @@ -447,7 +454,8 @@ let new_evar ?src ?filter ?abstract_arguments ?candidates ?naming ?typeclass_can match filter with | None -> instance | Some filter -> Filter.filter_list filter instance in - let (evd, evk) = new_pure_evar sign evd typ' ?src ?filter ?abstract_arguments ?candidates ?naming + let identity = if Int.equal (Environ.nb_rel env) 0 then Some instance else None in + let (evd, evk) = new_pure_evar sign evd typ' ?src ?filter ?identity ?abstract_arguments ?candidates ?naming ?typeclass_candidate ?principal in (evd, EConstr.mkEvar (evk, instance)) |