summaryrefslogtreecommitdiff
path: root/pretyping/pretype_errors.ml
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping/pretype_errors.ml')
-rw-r--r--pretyping/pretype_errors.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml
index 278a4761..856894d9 100644
--- a/pretyping/pretype_errors.ml
+++ b/pretyping/pretype_errors.ml
@@ -165,7 +165,7 @@ 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.empty, VarNotFound s)
+ raise_pretype_error ?loc (empty_env, Evd.from_env empty_env, VarNotFound s)
(*s Typeclass errors *)