From 9a431a1b43dead6d692c942986a25f0f8986465a Mon Sep 17 00:00:00 2001 From: herbelin Date: Thu, 28 Feb 2013 07:33:41 +0000 Subject: Repairing r16205: errors raised by check_evar_instance were no longer trapped by solve_simple_eqn. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16257 85f007b7-540e-0410-9357-904b9bb8a0f7 --- pretyping/evarsolve.mli | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) (limited to 'pretyping/evarsolve.mli') diff --git a/pretyping/evarsolve.mli b/pretyping/evarsolve.mli index e34332c9b..3e769e02d 100644 --- a/pretyping/evarsolve.mli +++ b/pretyping/evarsolve.mli @@ -54,5 +54,8 @@ val is_unification_pattern : env * int -> evar_map -> constr -> constr list -> val solve_pattern_eqn : env -> constr list -> constr -> constr -val check_evar_instance : evar_map -> existential_key -> constr -> conv_fun -> - evar_map +exception IllTypedInstance of env * types * types + +(* May raise IllTypedInstance if types are not convertible *) +val check_evar_instance : + evar_map -> existential_key -> constr -> conv_fun -> evar_map -- cgit v1.2.3