aboutsummaryrefslogtreecommitdiff
path: root/pretyping/pretype_errors.ml
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping/pretype_errors.ml')
-rw-r--r--pretyping/pretype_errors.ml3
1 files changed, 2 insertions, 1 deletions
diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml
index 4a60fce3d6..ef96bfb048 100644
--- a/pretyping/pretype_errors.ml
+++ b/pretyping/pretype_errors.ml
@@ -9,6 +9,7 @@
(* $Id$ *)
open Util
+open Stdpp
open Names
open Sign
open Term
@@ -137,7 +138,7 @@ let error_not_clean env sigma ev c =
raise (PretypeError (env_ise sigma env, NotClean (ev,c)))
let error_unsolvable_implicit loc env sigma e =
- raise (PretypeError (env_ise sigma env, UnsolvableImplicit e))
+ raise_with_loc loc (PretypeError (env_ise sigma env, UnsolvableImplicit e))
(*s Ml Case errors *)