diff options
Diffstat (limited to 'engine/evd.mli')
| -rw-r--r-- | engine/evd.mli | 23 |
1 files changed, 16 insertions, 7 deletions
diff --git a/engine/evd.mli b/engine/evd.mli index 87f74f660d..b0e3c2b869 100644 --- a/engine/evd.mli +++ b/engine/evd.mli @@ -139,7 +139,7 @@ val has_undefined : evar_map -> bool there are uninstantiated evars in [sigma]. *) val new_evar : evar_map -> - ?name:Id.t -> evar_info -> evar_map * Evar.t + ?name:Id.t -> ?typeclass_candidate:bool -> evar_info -> evar_map * Evar.t (** Creates a fresh evar mapping to the given information. *) val add : evar_map -> Evar.t -> evar_info -> evar_map @@ -176,7 +176,7 @@ val raw_map_undefined : (Evar.t -> evar_info -> evar_info) -> evar_map -> evar_m (** Same as {!raw_map}, but restricted to undefined evars. For efficiency reasons. *) -val define : Evar.t-> econstr -> evar_map -> evar_map +val define : Evar.t -> econstr -> evar_map -> evar_map (** Set the body of an evar to the given constr. It is expected that: {ul {- The evar is already present in the evarmap.} @@ -184,6 +184,10 @@ val define : Evar.t-> econstr -> evar_map -> evar_map {- All the evars present in the constr should be present in the evar map.} } *) +val define_with_evar : Evar.t -> econstr -> evar_map -> evar_map +(** Same as [define ev body evd], except the body must be an existential variable [ev']. + This additionally makes [ev'] inherit the [obligation] and [typeclass] flags of [ev]. *) + val cmap : (econstr -> econstr) -> evar_map -> evar_map (** Map the function on all terms in the evar map. *) @@ -204,6 +208,8 @@ val undefined_map : evar_map -> evar_info Evar.Map.t val drop_all_defined : evar_map -> evar_map +val is_maybe_typeclass_hook : (evar_map -> constr -> bool) Hook.t + (** {6 Instantiating partial terms} *) exception NotInstantiatedEvar @@ -244,13 +250,16 @@ val restrict : Evar.t-> Filter.t -> ?candidates:econstr list -> val is_restricted_evar : evar_map -> Evar.t -> Evar.t option (** Tell if an evar comes from restriction of another evar, and if yes, which *) -val set_resolvable_evar : evar_map -> Evar.t -> bool -> evar_map -(** Declare an evar resolvable or unresolvable for typeclass resolution *) +val set_typeclass_evars : evar_map -> Evar.Set.t -> evar_map +(** Mark the given set of evars as available for resolution. + + Precondition: they should indeed refer to undefined typeclass evars. + *) -val unresolvable_evars : evar_map -> Evar.Set.t -(** The set of unresolvable evars *) +val get_typeclass_evars : evar_map -> Evar.Set.t +(** The set of undefined typeclass evars *) -val is_resolvable_evar : evar_map -> Evar.t -> bool +val is_typeclass_evar : evar_map -> Evar.t -> bool (** Is the evar declared resolvable for typeclass resolution *) val set_obligation_evar : evar_map -> Evar.t -> evar_map |