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.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml
index 856894d9a6..01b0d96f98 100644
--- a/pretyping/pretype_errors.ml
+++ b/pretyping/pretype_errors.ml
@@ -164,8 +164,8 @@ let error_not_product ?loc env sigma c =
(*s Error in conversion from AST to glob_constr *)
-let error_var_not_found ?loc s =
- raise_pretype_error ?loc (empty_env, Evd.from_env empty_env, VarNotFound s)
+let error_var_not_found ?loc env sigma s =
+ raise_pretype_error ?loc (env, sigma, VarNotFound s)
(*s Typeclass errors *)