From b679eae9d3588f6cb91be174ab80a64fb5c434a4 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 13 May 2016 17:41:23 +0200
Subject: More informative error message when interpreting ltac variables in
 terms.

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

diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 21eb100b4e..5d1f77a5a2 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -389,9 +389,12 @@ let pretype_id pretype k0 loc env evdref lvar id =
     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 lvar.ltac_genargs then
+      if Id.Map.mem id lvar.ltac_genargs then begin
+        let Geninterp.Val.Dyn (typ, _) = Id.Map.find id lvar.ltac_genargs in
 	user_err_loc (loc,"",
-          str "Variable " ++ pr_id id ++ str " should be bound to a term.");
+          str "Variable " ++ pr_id id ++ str " should be bound to a term but is \
+          bound to a " ++ Geninterp.Val.pr typ ++ str ".")
+      end;
       (* Check if [id] is a section or goal variable *)
       try
 	  { uj_val  = mkVar id; uj_type = (get_type (lookup_named id env)) }
-- 
cgit v1.2.3