From 56744aadd413dd9417d245951083117b05170e14 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 22 Oct 2016 11:38:51 +0200
Subject: Fixing printing of generic arguments of tag "var".

---
 tactics/tacinterp.ml       | 3 +++
 test-suite/output/ltac.out | 1 +
 test-suite/output/ltac.v   | 5 +++++
 3 files changed, 9 insertions(+)

diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 5ecc46d670..c3f7fa1439 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -816,6 +816,9 @@ let rec message_of_value v =
       Ftactic.return (pr_closed_glob_env (pf_env gl)
                         (Proofview.Goal.sigma gl) c)
     end
+  else if has_type v (topwit wit_var) then
+    let id = out_gen (topwit wit_var) v in
+    Ftactic.nf_enter begin fun gl -> Ftactic.return (pr_id id) end
   else match Value.to_list v with
   | Some l ->
     Ftactic.List.map message_of_value l >>= fun l ->
diff --git a/test-suite/output/ltac.out b/test-suite/output/ltac.out
index d003c70df9..266e4c7243 100644
--- a/test-suite/output/ltac.out
+++ b/test-suite/output/ltac.out
@@ -1,2 +1,3 @@
 The command has indeed failed with message:
 Error: Ltac variable y depends on pattern variable name z which is not bound in current context.
+Hx
diff --git a/test-suite/output/ltac.v b/test-suite/output/ltac.v
index 7e2610c7d7..e5bcff8ddb 100644
--- a/test-suite/output/ltac.v
+++ b/test-suite/output/ltac.v
@@ -15,3 +15,8 @@ lazymatch goal with
 | H1 : HT |- _ => idtac
 end.
 Abort.
+
+(* Check printing of the "var" argument "Hx" *)
+Ltac m H := idtac H; exact H.
+Goal True.
+let a:=constr:(let Hx := 0 in ltac:(m Hx)) in idtac.
-- 
cgit v1.2.3