Distinguish globalization and pretyping error on unbound variable

We can then avoid passing an empty env.

4 files changed, 7 insertions, 8 deletions

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)
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 *)
 
diff --git a/pretyping/pretype_errors.mli b/pretyping/pretype_errors.mli
index 6f14d025c7..054f0c76a9 100644
--- a/pretyping/pretype_errors.mli
+++ b/pretyping/pretype_errors.mli
@@ -150,9 +150,7 @@ val error_unexpected_type :
 val error_not_product :
   ?loc:Loc.t -> env -> Evd.evar_map -> constr -> 'b
 
-(** {6 Error in conversion from AST to glob_constr } *)
-
-val error_var_not_found : ?loc:Loc.t -> Id.t -> 'b
+val error_var_not_found : ?loc:Loc.t -> env -> Evd.evar_map -> Id.t -> 'b
 
 (** {6 Typeclass errors } *)
 
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 37afcf75e1..55817f1b76 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -390,7 +390,7 @@ let pretype_id pretype k0 loc env sigma id =
     sigma, { uj_val  = mkVar id; uj_type = NamedDecl.get_type (lookup_named id !!env) }
   with Not_found ->
     (* [id] not found, standard error message *)
-    error_var_not_found ?loc id
+    error_var_not_found ?loc !!env sigma id
 
 (*************************************************************************)
 (* Main pretyping function                                               *)
@@ -436,7 +436,7 @@ let pretype_ref ?loc sigma env ref us =
          (* This may happen if env is a goal env and section variables have
             been cleared - section variables should be different from goal
             variables *)
-         Pretype_errors.error_var_not_found ?loc id)
+         Pretype_errors.error_var_not_found ?loc !!env sigma id)
   | ref ->
     let sigma, c = pretype_global ?loc univ_flexible env sigma ref us in
     let ty = unsafe_type_of !!env sigma c in