1 files changed, 10 insertions, 0 deletions
diff --git a/test-suite/output/ltac.v b/test-suite/output/ltac.v
index 7e2610c7d..373b870b9 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.