From f8f2c684ce97745350f8cbcb654a2ee27fb9d572 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 9 Apr 2016 18:18:46 +0200
Subject: A small test of Print Ltac.

---
 test-suite/output/ltac.out |  3 +++
 test-suite/output/ltac.v   | 10 ++++++++++
 2 files changed, 13 insertions(+)

diff --git a/test-suite/output/ltac.out b/test-suite/output/ltac.out
index d003c70df9..20e274e254 100644
--- a/test-suite/output/ltac.out
+++ b/test-suite/output/ltac.out
@@ -1,2 +1,5 @@
 The command has indeed failed with message:
 Error: Ltac variable y depends on pattern variable name z which is not bound in current context.
+Ltac f x y z :=
+  symmetry in x, y; auto with z; auto; intros **; clearbody x; generalize
+   dependent z
diff --git a/test-suite/output/ltac.v b/test-suite/output/ltac.v
index 7e2610c7d7..373b870b9f 100644
--- a/test-suite/output/ltac.v
+++ b/test-suite/output/ltac.v
@@ -15,3 +15,13 @@ lazymatch goal with
 | H1 : HT |- _ => idtac
 end.
 Abort.
+
+Ltac f x y z :=
+  symmetry in x, y;
+  auto with z;
+  auto;
+  intros;
+  clearbody x;
+  generalize dependent z.
+
+Print Ltac f.
-- 
cgit v1.2.3