Merge PR #6113: Extra work on ltac printing: fixing #5787, some parentheses

2 files changed, 18 insertions, 0 deletions

diff --git a/test-suite/output/ltac.out b/test-suite/output/ltac.out
index 35c3057d84..c5d58ec1ec 100644
--- a/test-suite/output/ltac.out
+++ b/test-suite/output/ltac.out
@@ -31,3 +31,10 @@ nat
 nat
 0
 0
+Ltac foo :=
+  let x := intros ** in
+  let y := intros -> in
+  let v := constr:(nil) in
+  let w := () in
+  let z := 1 in
+  pose v
diff --git a/test-suite/output/ltac.v b/test-suite/output/ltac.v
index 76c37625aa..6adbe95dd5 100644
--- a/test-suite/output/ltac.v
+++ b/test-suite/output/ltac.v
@@ -57,3 +57,14 @@ match goal with |- ?x*?y => idtac x end.
 match goal with H: context [?x*?y] |- _ => idtac x end.
 match goal with |- context [?x*?y] => idtac x end.
 Abort.
+
+(* Check printing of let in Ltac and Tactic Notation *)
+
+Ltac foo :=
+  let x := intros in
+  let y := intros -> in
+  let v := constr:(@ nil True) in
+  let w := () in
+  let z := 1 in
+  pose v.
+Print Ltac foo.