Imported Upstream version 8.8.2upstream/8.8.2

1 files changed, 11 insertions, 0 deletions

diff --git a/test-suite/output/ltac.v b/test-suite/output/ltac.v
index 76c37625..6adbe95d 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.