From 1161ccf74578c3190d296dc37f39edecf28cf078 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Tue, 7 Nov 2017 15:20:53 +0100
Subject: Printing again "intros  **" as "intros" by default.

The rationale it that it is more common to do so and thus more
"natural" (principle of writing less whenever possible).
---
 test-suite/output/ltac.out | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'test-suite')

diff --git a/test-suite/output/ltac.out b/test-suite/output/ltac.out
index 7f3cdad6ce..eb9f571022 100644
--- a/test-suite/output/ltac.out
+++ b/test-suite/output/ltac.out
@@ -1,7 +1,7 @@
 The command has indeed failed with message:
 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
+  symmetry in x, y; auto with z; auto; intros; clearbody x; generalize
    dependent z
 The command has indeed failed with message:
 In nested Ltac calls to "g1" and "refine (uconstr)", last call failed.
-- 
cgit v1.2.3