diff options
Diffstat (limited to 'engine/evd.mli')
| -rw-r--r-- | engine/evd.mli | 14 |
1 files changed, 9 insertions, 5 deletions
diff --git a/engine/evd.mli b/engine/evd.mli index 405fcc403..db2bd4eed 100644 --- a/engine/evd.mli +++ b/engine/evd.mli @@ -113,6 +113,7 @@ val evar_filtered_context : evar_info -> (econstr, etypes) Context.Named.pt val evar_hyps : evar_info -> named_context_val val evar_filtered_hyps : evar_info -> named_context_val val evar_body : evar_info -> evar_body +val evar_candidates : evar_info -> constr list option val evar_filter : evar_info -> Filter.t val evar_env : evar_info -> env val evar_filtered_env : evar_info -> env @@ -229,7 +230,7 @@ val existential_opt_value : evar_map -> econstr pexistential -> econstr option val existential_opt_value0 : evar_map -> existential -> constr option -val evar_instance_array : (Context.Named.Declaration.t -> 'a -> bool) -> evar_info -> +val evar_instance_array : (Constr.named_declaration -> 'a -> bool) -> evar_info -> 'a array -> (Id.t * 'a) list val instantiate_evar_array : evar_info -> econstr -> econstr array -> econstr @@ -243,7 +244,8 @@ val evars_reset_evd : ?with_conv_pbs:bool -> ?with_univs:bool -> val restrict : Evar.t-> Filter.t -> ?candidates:econstr list -> ?src:Evar_kinds.t located -> evar_map -> evar_map * Evar.t (** Restrict an undefined evar into a new evar by filtering context and - possibly limiting the instances to a set of candidates *) + possibly limiting the instances to a set of candidates (candidates + are filtered according to the filter) *) val is_restricted_evar : evar_info -> Evar.t option (** Tell if an evar comes from restriction of another evar, and if yes, which *) @@ -338,8 +340,6 @@ val shelve_on_future_goals : Evar.t list -> future_goals -> future_goals Evar maps also keep track of the universe constraints defined at a given point. This section defines the relevant manipulation functions. *) -val whd_sort_variable : evar_map -> econstr -> econstr - exception UniversesDiffer val add_universe_constraints : evar_map -> UnivProblem.Set.t -> evar_map @@ -439,7 +439,11 @@ type clbinding = (** Unification constraints *) type conv_pb = Reduction.conv_pb type evar_constraint = conv_pb * env * econstr * econstr + +(** The following two functions are for internal use only, + see [Evarutil.add_unification_pb] for a safe interface. *) val add_conv_pb : ?tail:bool -> evar_constraint -> evar_map -> evar_map +val conv_pbs : evar_map -> evar_constraint list val extract_changed_conv_pbs : evar_map -> (Evar.Set.t -> evar_constraint -> bool) -> @@ -592,7 +596,7 @@ val update_sigma_env : evar_map -> env -> evar_map (** Polymorphic universes *) -val fresh_sort_in_family : ?loc:Loc.t -> ?rigid:rigid -> env -> evar_map -> Sorts.family -> evar_map * Sorts.t +val fresh_sort_in_family : ?loc:Loc.t -> ?rigid:rigid -> evar_map -> Sorts.family -> evar_map * Sorts.t val fresh_constant_instance : ?loc:Loc.t -> env -> evar_map -> Constant.t -> evar_map * pconstant val fresh_inductive_instance : ?loc:Loc.t -> env -> evar_map -> inductive -> evar_map * pinductive val fresh_constructor_instance : ?loc:Loc.t -> env -> evar_map -> constructor -> evar_map * pconstructor |