diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/evarconv.ml | 7 | ||||
| -rw-r--r-- | pretyping/evarsolve.mli | 12 |
2 files changed, 14 insertions, 5 deletions
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index cbf539c1e9..00d4c7b3d8 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -1620,12 +1620,15 @@ let apply_conversion_problem_heuristic flags env evd with_ho pbty t1 t2 = in Success (solve_refl ~can_drop:true f flags env evd (position_problem true pbty) evk1 args1 args2) - | Evar ev1, Evar ev2 when app_empty -> + | Evar (evk1,_ as ev1), Evar ev2 when app_empty -> (* solve_evar_evar handles the cases ev1 and/or ev2 are frozen *) - Success (solve_evar_evar ~force:true + (try + Success (solve_evar_evar ~force:true (evar_define evar_unify flags ~choose:true) evar_unify flags env evd (position_problem true pbty) ev1 ev2) + with IllTypedInstance (env,t,u) -> + UnifFailure (evd,InstanceNotSameType (evk1,env,t,u))) | Evar ev1,_ when is_evar_allowed flags (fst ev1) && Array.length l1 <= Array.length l2 -> (* On "?n t1 .. tn = u u1 .. u(n+p)", try first-order unification *) (* and otherwise second-order matching *) diff --git a/pretyping/evarsolve.mli b/pretyping/evarsolve.mli index 8ff2d7fc63..094dae4828 100644 --- a/pretyping/evarsolve.mli +++ b/pretyping/evarsolve.mli @@ -99,7 +99,9 @@ type conversion_check = unify_flags -> unification_kind -> Preconditions: - [ev] does not occur in [c]. - [c] does not contain any Meta(_) - *) + + If [ev] and [c] have non inferably convertible types, an exception + [IllTypedInstance] is raised *) val instantiate_evar : unifier -> unify_flags -> env -> evar_map -> Evar.t -> constr -> evar_map @@ -107,7 +109,9 @@ val instantiate_evar : unifier -> unify_flags -> env -> evar_map -> (** [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 (except if choose is - true); fails if the instance is not valid for the given [ev] *) + true); fails if the instance is not valid for the given [ev]; + If [ev] and [c] have non inferably convertible types, an exception + [IllTypedInstance] is raised *) val evar_define : unifier -> unify_flags -> ?choose:bool -> ?imitate_defs:bool -> env -> evar_map -> bool option -> existential -> constr -> evar_map @@ -129,6 +133,8 @@ val solve_evar_evar : ?force:bool -> (env -> evar_map -> bool option -> existential -> constr -> evar_map) -> unifier -> unify_flags -> env -> evar_map -> bool option -> existential -> existential -> evar_map + (** The two evars are expected to be in inferably convertible types; + if not, an exception IllTypedInstance is raised *) val solve_simple_eqn : unifier -> unify_flags -> ?choose:bool -> ?imitate_defs:bool -> env -> evar_map -> bool option * existential * constr -> unification_result @@ -147,9 +153,9 @@ val noccur_evar : env -> evar_map -> Evar.t -> constr -> bool exception IllTypedInstance of env * types * types -(* May raise IllTypedInstance if types are not convertible *) val check_evar_instance : unifier -> unify_flags -> env -> evar_map -> Evar.t -> constr -> evar_map + (** May raise IllTypedInstance if types are not convertible *) val remove_instance_local_defs : evar_map -> Evar.t -> 'a list -> 'a list |