5 files changed, 101 insertions, 0 deletions
diff --git a/test-suite/dune b/test-suite/dune
new file mode 100644
index 0000000000..c5fa0bb14a
--- /dev/null
+++ b/test-suite/dune
@@ -0,0 +1,73 @@
+(rule
+ (targets summary.log)
+ (deps
+   ; File that should be promoted.
+   misc/universes/all_stdlib.v
+   ; Dependencies of the legacy makefile
+   ../Makefile.common
+   ../config/Makefile
+   ; Stuff for the compat script test
+   ../dev/header.ml
+   ../dev/tools/update-compat.py
+   ../doc/stdlib/index-list.html.template
+   (package coq)
+   ; For fake_ide
+   (package coqide-server)
+   (source_tree .))
+   ; Finer-grained dependencies look like this
+   ; ../tools/CoqMakefile.in
+   ; ../theories/Init/Prelude.vo
+   ; ../theories/Arith/Arith.vo
+   ; ../theories/Arith/Compare.vo
+   ; ../theories/PArith/PArith.vo
+   ; ../theories/QArith/QArith.vo
+   ; ../theories/QArith/Qcanon.vo
+   ; ../theories/ZArith/ZArith.vo
+   ; ../theories/ZArith/Zwf.vo
+   ; ../theories/Sets/Ensembles.vo
+   ; ../theories/Numbers/Natural/Peano/NPeano.vo
+   ; ../theories/Numbers/Cyclic/Int31/Cyclic31.vo
+   ; ../theories/FSets/FMaps.vo
+   ; ../theories/FSets/FSets.vo
+   ; ../theories/MSets/MSets.vo
+   ; ../theories/Compat/Coq87.vo
+   ; ../theories/Compat/Coq88.vo
+   ; ../theories/Relations/Relations.vo
+   ; ../theories/Unicode/Utf8.vo
+   ; ../theories/Program/Program.vo
+   ; ../theories/Classes/EquivDec.vo
+   ; ../theories/Classes/DecidableClass.vo
+   ; ../theories/Classes/SetoidClass.vo
+   ; ../theories/Classes/RelationClasses.vo
+   ; ../theories/Logic/Classical.vo
+   ; ../theories/Logic/Hurkens.vo
+   ; ../theories/Logic/ClassicalFacts.vo
+   ; ../theories/Reals/Reals.vo
+   ; ../theories/Lists/Streams.vo
+   ; ../plugins/micromega/Lia.vo
+   ; ../plugins/micromega/Lqa.vo
+   ; ../plugins/micromega/Psatz.vo
+   ; ../plugins/micromega/MExtraction.vo
+   ; ../plugins/nsatz/Nsatz.vo
+   ; ../plugins/omega/Omega.vo
+   ; ../plugins/ssr/ssrbool.vo
+   ; ../plugins/derive/Derive.vo
+   ; ../plugins/funind/Recdef.vo
+   ; ../plugins/extraction/Extraction.vo
+   ; ../plugins/extraction/ExtrOcamlNatInt.vo
+   ; coqtop
+   ; coqtop.opt
+   ; coqidetop.opt
+   ; coqqueryworker.opt
+   ; coqtacticworker.opt
+   ; coqproofworker.opt
+   ; coqc
+   ; coqchk
+   ; coqdoc
+   ; %{bin:coq_makefile}
+   ; %{bin:fake_ide}
+ (action
+  (progn
+   ; XXX: we will allow to set the NJOBS variable in a future Dune
+   ; version, either by using an env var or by letting Dune set `-j`
+   (run make -j 2 BIN= PRINT_LOGS=1))))
diff --git a/test-suite/misc/universes/build_all_stdlib.sh b/test-suite/misc/universes/build_all_stdlib.sh
new file mode 100755
index 0000000000..2d2e6f863b
--- /dev/null
+++ b/test-suite/misc/universes/build_all_stdlib.sh
@@ -0,0 +1,4 @@
+#!/usr/bin/env bash
+
+echo "Require $(find ../../../theories ../../../plugins -type f -name "*.v" | \
+        sed 's/^.*\/theories\///' | sed 's/^.*\/plugins\///' | sed 's/\.v$//' | sed 's/\//./g') ."
diff --git a/test-suite/misc/universes/dune b/test-suite/misc/universes/dune
new file mode 100644
index 0000000000..58bba300d2
--- /dev/null
+++ b/test-suite/misc/universes/dune
@@ -0,0 +1,8 @@
+(rule
+ (targets all_stdlib.v)
+ (deps
+   (source_tree ../../../theories)
+   (source_tree ../../../plugins))
+ (action
+   (with-outputs-to all_stdlib.v
+    (run ./build_all_stdlib.sh))))
diff --git a/test-suite/output/PrintModule.out b/test-suite/output/PrintModule.out
index 751d5fcc48..1a9bc068c5 100644
--- a/test-suite/output/PrintModule.out
+++ b/test-suite/output/PrintModule.out
@@ -1,5 +1,9 @@
 Module N : S with Definition T := nat := M
 
+Module N : S with Definition T := M
+
 Module N : S with Module T := K := M
 
+Module N : S with Module T := M
+
 Module Type Func = Funsig (T0:Test) Sig Parameter x : T0.t. End
diff --git a/test-suite/output/PrintModule.v b/test-suite/output/PrintModule.v
index 5f30f7cda6..54ef305be4 100644
--- a/test-suite/output/PrintModule.v
+++ b/test-suite/output/PrintModule.v
@@ -1,3 +1,5 @@
+(* Bug #2169 *)
+
 Module FOO.
 
 Module M.
@@ -12,6 +14,10 @@ Module N : S with Definition T := nat := M.
 
 Print Module N.
 
+Set Short Module Printing.
+Print Module N.
+Unset Short Module Printing.
+
 End FOO.
 
 Module BAR.
@@ -31,8 +37,14 @@ Module N : S with Module T := K := M.
 
 Print Module N.
 
+Set Short Module Printing.
+Print Module N.
+Unset Short Module Printing.
+
 End BAR.
 
+(* Bug #4661 *)
+
 Module QUX.
 
 Module Type Test.