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.
---
 plugins/ltac/tacintern.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'plugins')

diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml
index 55412c74bb..a2b4156f50 100644
--- a/plugins/ltac/tacintern.ml
+++ b/plugins/ltac/tacintern.ml
@@ -83,7 +83,8 @@ let intern_hyp ist ({loc;v=id} as locid) =
   else if find_ident id ist then
     make id
   else
-    Pretype_errors.error_var_not_found ?loc id
+    CErrors.user_err ?loc Pp.(str "Hypothesis" ++ spc () ++ Id.print id ++ spc() ++
+                              str "was not found in the current environment.")
 
 let intern_or_var f ist = function
   | ArgVar locid -> ArgVar (intern_hyp ist locid)
-- 
cgit v1.2.3