From 6214079b980b8a02bef20d5b25abbe49c3095f32 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Tue, 30 Oct 2018 11:03:26 +0100
Subject: Distinguish globalization and pretyping error on unbound variable

We can then avoid passing an empty env.
---
 pretyping/pretype_errors.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'pretyping/pretype_errors.ml')

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 *)
 
-- 
cgit v1.2.3