5 files changed, 37 insertions, 2 deletions
diff --git a/test-suite/Makefile b/test-suite/Makefile
index 7a204bfd8..f169f86e8 100644
--- a/test-suite/Makefile
+++ b/test-suite/Makefile
@@ -174,7 +174,7 @@ summary.log:
 # if not on travis we can get the log files (they're just there for a
 # local build, and downloadable on GitLab)
 report: summary.log
-	$(HIDE)./save-logs.sh
+	$(HIDE)bash save-logs.sh
 	$(HIDE)if [ -n "${TRAVIS}" ]; then find logs/ -name '*.log' -not -name 'summary.log' -exec 'bash' '-c' 'echo "travis_fold:start:coq.logs.$$(echo '{}' | sed s,/,.,g)"' ';' -exec cat '{}' ';' -exec 'bash' '-c' 'echo "travis_fold:end:coq.logs.$$(echo '{}' | sed s,/,.,g)"' ';'; fi
 	$(HIDE)if [ -n "${APPVEYOR}" ]; then find logs/ -name '*.log' -not -name 'summary.log' -exec 'bash' '-c' 'echo {}' ';' -exec cat '{}' ';' -exec 'bash' '-c' 'echo' ';'; fi
 	$(HIDE)if grep -q -F 'Error!' summary.log ; then echo FAILURES; grep -F 'Error!' summary.log; false; else echo NO FAILURES; fi
@@ -528,7 +528,7 @@ coq-makefile/%.log : coq-makefile/%/run.sh
 	$(HIDE)(\
 	  export COQBIN=$(BIN);\
 	  cd coq-makefile/$* && \
-	  ./run.sh 2>&1; \
+	  bash run.sh 2>&1; \
 	if [ $$? = 0 ]; then \
 	    echo $(log_success); \
 	    echo "    $<...Ok"; \
diff --git a/test-suite/bugs/closed/5790.v b/test-suite/bugs/closed/5790.v
new file mode 100644
index 000000000..6c93a3906
--- /dev/null
+++ b/test-suite/bugs/closed/5790.v
@@ -0,0 +1,7 @@
+Set Universe Polymorphism.
+Section foo.
+Context (v : Type).
+Axiom a : True <-> False.
+
+Hint Resolve -> a.
+End foo.
diff --git a/test-suite/coq-makefile/timing/run.sh b/test-suite/coq-makefile/timing/run.sh
index 7e0baaa8f..2428da731 100755
--- a/test-suite/coq-makefile/timing/run.sh
+++ b/test-suite/coq-makefile/timing/run.sh
@@ -41,6 +41,9 @@ for ext in "" .desired; do
     done
 done
 for file in time-of-build-before.log time-of-build-after.log time-of-build-both.log; do
+    echo "cat $file"
+    cat "$file"
+    echo
     diff -u $file.desired.processed $file.processed || exit $?
 done
 
@@ -56,6 +59,13 @@ make all TIMING=after -j2 || exit $?
 
 find ../per-file-before/ -name "*.before-timing" -exec 'cp' '{}' './' ';'
 make all.timing.diff -j2 || exit $?
+echo "cat A.v.before-timing"
+cat A.v.before-timing
+echo
+echo "cat A.v.after-timing"
+cat A.v.after-timing
+echo
+echo "cat A.v.timing.diff"
 cat A.v.timing.diff
 echo
 
diff --git a/test-suite/output/ltac.out b/test-suite/output/ltac.out
index 35c3057d8..c5d58ec1e 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 76c37625a..6adbe95dd 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.