diff options
Diffstat (limited to 'pretyping/evd.mli')
| -rw-r--r-- | pretyping/evd.mli | 14 |
1 files changed, 4 insertions, 10 deletions
diff --git a/pretyping/evd.mli b/pretyping/evd.mli index 53f8b0db..fe785a83 100644 --- a/pretyping/evd.mli +++ b/pretyping/evd.mli @@ -12,7 +12,6 @@ open Names open Term open Context open Environ -open Mod_subst (** {5 Existential variables and unification states} @@ -127,10 +126,6 @@ type evar_map (** Type of unification state. Essentially a bunch of state-passing data needed to handle incremental term construction. *) -val progress_evar_map : evar_map -> evar_map -> bool -(** Assuming that the second map extends the first one, this says if - some existing evar has been refined *) - val empty : evar_map (** The empty evar map. *) @@ -205,9 +200,6 @@ val add_constraints : evar_map -> Univ.constraints -> evar_map val undefined_map : evar_map -> evar_info Evar.Map.t (** Access the undefined evar mapping directly. *) -val eq_evar_info : evar_map -> evar_info -> evar_info -> bool -(** Compare the evar_info's up to the universe constraints of the evar map. *) - val drop_all_defined : evar_map -> evar_map (** {6 Instantiating partial terms} *) @@ -224,7 +216,7 @@ val existential_opt_value : evar_map -> existential -> constr option (** Same as {!existential_value} but returns an option instead of raising an exception. *) -val evar_instance_array : (Id.t -> 'a -> bool) -> evar_info -> +val evar_instance_array : (named_declaration -> 'a -> bool) -> evar_info -> 'a array -> (Id.t * 'a) list val instantiate_evar_array : evar_info -> constr -> constr array -> constr @@ -398,7 +390,7 @@ type clbinding = (** Unification constraints *) type conv_pb = Reduction.conv_pb type evar_constraint = conv_pb * env * constr * constr -val add_conv_pb : evar_constraint -> evar_map -> evar_map +val add_conv_pb : ?tail:bool -> evar_constraint -> evar_map -> evar_map val extract_changed_conv_pbs : evar_map -> (Evar.Set.t -> evar_constraint -> bool) -> @@ -538,6 +530,8 @@ val with_context_set : rigid -> evar_map -> 'a Univ.in_universe_context_set -> e val nf_univ_variables : evar_map -> evar_map * Univ.universe_subst val abstract_undefined_variables : evar_universe_context -> evar_universe_context +val fix_undefined_variables : evar_map -> evar_map + val refresh_undefined_universes : evar_map -> evar_map * Univ.universe_level_subst val nf_constraints : evar_map -> evar_map |