diff options
Diffstat (limited to 'pretyping/evd.mli')
| -rw-r--r-- | pretyping/evd.mli | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/pretyping/evd.mli b/pretyping/evd.mli index e1fc425b..ef6a3d7b 100644 --- a/pretyping/evd.mli +++ b/pretyping/evd.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: evd.mli 9573 2007-01-31 20:18:18Z notin $ i*) +(*i $Id: evd.mli 9976 2007-07-12 11:58:30Z msozeau $ i*) (*i*) open Util @@ -111,8 +111,8 @@ val map_clb : (constr -> constr) -> clbinding -> clbinding (* Unification state *) type evar_defs -(* Substitution is not applied to the [evar_map] *) -val subst_evar_defs : substitution -> evar_defs -> evar_defs +(* Assume empty [evar_map] and [conv_pbs] *) +val subst_evar_defs_light : substitution -> evar_defs -> evar_defs (* create an [evar_defs] with empty meta map: *) val create_evar_defs : evar_map -> evar_defs @@ -123,7 +123,7 @@ val evars_reset_evd : evar_map -> evar_defs -> evar_defs type hole_kind = | ImplicitArg of global_reference * (int * identifier option) | BinderType of name - | QuestionMark + | QuestionMark of bool (* Can it be turned into an obligation ? *) | CasesType | InternalHole | TomatchTypeParameter of inductive * int @@ -138,7 +138,7 @@ val evar_source : existential_key -> evar_defs -> loc * hole_kind (* Unification constraints *) type conv_pb = Reduction.conv_pb -type evar_constraint = conv_pb * constr * constr +type evar_constraint = conv_pb * Environ.env * constr * constr val add_conv_pb : evar_constraint -> evar_defs -> evar_defs val get_conv_pbs : evar_defs -> (evar_constraint -> bool) -> evar_defs * evar_constraint list |