aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/evarconv.mli
diff options
context:
space:
mode:
authorGravatar msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7>2010-03-07 18:49:23 +0000
committerGravatar msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7>2010-03-07 18:49:23 +0000
commitc14f134c00cef3dbca8c4a66f9847094f3fd119c (patch)
tree8d30a07075934e758e21115d6b5b941e8c716bda /pretyping/evarconv.mli
parentba360bdefa2d7e4200c94a37c5065019718c2691 (diff)
Fix treatment of remaining unification constraints: raise a more
informative exception if some constraints do not unify. All calls except one used to raise a less informative exception when the constraints weren't solved. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12849 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping/evarconv.mli')
-rw-r--r--pretyping/evarconv.mli2
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/evarconv.mli b/pretyping/evarconv.mli
index 9a4247bc2..28b960bb9 100644
--- a/pretyping/evarconv.mli
+++ b/pretyping/evarconv.mli
@@ -34,7 +34,7 @@ val evar_eqappr_x :
evar_map * bool
(*i*)
-val consider_remaining_unif_problems : env -> evar_map -> evar_map * bool
+val consider_remaining_unif_problems : env -> evar_map -> evar_map
val check_conv_record : constr * types list -> constr * types list ->
constr * constr list * (constr list * constr list) *