diff options
Diffstat (limited to 'pretyping/evarutil.mli')
| -rw-r--r-- | pretyping/evarutil.mli | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli index a687fdf0..cb54f400 100644 --- a/pretyping/evarutil.mli +++ b/pretyping/evarutil.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: evarutil.mli 11745 2009-01-04 18:43:08Z herbelin $ i*) +(*i $Id: evarutil.mli 12053 2009-04-06 16:20:42Z msozeau $ i*) (*i*) open Util @@ -53,11 +53,11 @@ val make_pure_subst : evar_info -> constr array -> (identifier * constr) list (***********************************************************) (* Instantiate evars *) -(* [evar_define env ev c] try to instantiate [ev] with [c] (typed in [env]), +(* [evar_define choose env ev c] try to instantiate [ev] with [c] (typed in [env]), possibly solving related unification problems, possibly leaving open - some problems that cannot be solved in a unique way; - failed if the instance is not valid for the given [ev] *) -val evar_define : env -> existential -> constr -> evar_defs -> evar_defs + some problems that cannot be solved in a unique way (except if choose is + true); fails if the instance is not valid for the given [ev] *) +val evar_define : ?choose:bool -> env -> existential -> constr -> evar_defs -> evar_defs (***********************************************************) (* Evars/Metas switching... *) @@ -80,7 +80,7 @@ val solve_refl : evar_defs val solve_simple_eqn : (env -> evar_defs -> conv_pb -> constr -> constr -> evar_defs * bool) - -> env -> evar_defs -> conv_pb * existential * constr -> + -> ?choose:bool -> env -> evar_defs -> conv_pb * existential * constr -> evar_defs * bool (* [check_evars env initial_sigma extended_sigma c] fails if some |