From e59d58b6db222332f7d7ad2adcb2b78c24fb351e Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Tue, 7 Nov 2017 15:24:16 +0100
Subject: Fixes #5787 (printing of "constr:" lost in the move of constr to
 Generic).

Was broken since 8.6.
---
 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 c5d58ec1ec..7f3cdad6ce 100644
--- a/test-suite/output/ltac.out
+++ b/test-suite/output/ltac.out
@@ -32,7 +32,7 @@ nat
 0
 0
 Ltac foo :=
-  let x := intros ** in
+  let x := intros in
   let y := intros -> in
   let v := constr:(nil) in
   let w := () in
-- 
cgit v1.2.3


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