From 8c3455e2f5db09e70cd7a40a96856f5be79adaff Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 5 Apr 2014 13:14:35 +0200
Subject: Fixing bug #3228 (fixing precedence of ltac variables over variables
 in env).

---
 pretyping/pretyping.ml | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

(limited to 'pretyping')

diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index def8dbfb1d..c66221e5f7 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -249,16 +249,16 @@ let pretype_id loc env sigma (lvar,unbndltacvars) id =
       let c = substl subst c in
 	{ uj_val = c; uj_type = protected_get_type_of env sigma c }
     with Not_found ->
+        (* Check if [id] is a ltac variable not bound to a term *)
+	(* and build a nice error message *)
+      if Id.Map.mem id unbndltacvars then
+	user_err_loc (loc,"",
+          str "Variable " ++ pr_id id ++ str " should be bound to a term.");
       (* Check if [id] is a section or goal variable *)
       try
 	let (_,_,typ) = lookup_named id env in
 	  { uj_val  = mkVar id; uj_type = typ }
       with Not_found ->
-	(* [id] not found, build nice error message if [id] yet known from ltac *)
-	if Id.Map.mem id unbndltacvars then
-	  user_err_loc (loc,"",
-            str "Variable " ++ pr_id id ++ str " should be bound to a term.")
-        else
 	  (* [id] not found, standard error message *)
 	  error_var_not_found_loc loc id
 
-- 
cgit v1.2.3