From f3db9d5424d411205c3fdde6d5b7ef11399de691 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sun, 7 Nov 2010 23:33:13 +0000
Subject: Add information of localisation when an error involving an "implicit
 types" occurs. Also improved the "unexpected type" error message.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13626 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 plugins/subtac/subtac_command.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins')

diff --git a/plugins/subtac/subtac_command.ml b/plugins/subtac/subtac_command.ml
index 7c6e54a9ca..8527766305 100644
--- a/plugins/subtac/subtac_command.ml
+++ b/plugins/subtac/subtac_command.ml
@@ -86,7 +86,7 @@ let interp_constr_judgment isevars env c =
 let locate_if_isevar loc na = function
   | RHole _ ->
       (try match na with
-	| Name id ->  Reserve.find_reserved_type id
+	| Name id -> rawconstr_of_aconstr loc (Reserve.find_reserved_type id)
 	| Anonymous -> raise Not_found
       with Not_found -> RHole (loc, Evd.BinderType na))
   | x -> x
-- 
cgit v1.2.3