2 files changed, 6 insertions, 0 deletions
diff --git a/test-suite/output/ltac.out b/test-suite/output/ltac.out
index f4254e4e2f..a62f4312ed 100644
--- a/test-suite/output/ltac.out
+++ b/test-suite/output/ltac.out
@@ -26,3 +26,4 @@ The command has indeed failed with message:
 In nested Ltac calls to "h" and "injection (destruction_arg)", last call
 failed.
 Error: No primitive equality found.
+Hx
diff --git a/test-suite/output/ltac.v b/test-suite/output/ltac.v
index dfa60eeda0..fb1dab7994 100644
--- a/test-suite/output/ltac.v
+++ b/test-suite/output/ltac.v
@@ -43,3 +43,8 @@ Goal True -> False.
 Fail h I.
 intro H.
 Fail h H.
+
+(* 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.