13 files changed, 129 insertions, 12 deletions
diff --git a/test-suite/.csdp.cache b/test-suite/.csdp.cache
index bd88c06d11..b85258505b 100644
--- a/test-suite/.csdp.cache
+++ b/test-suite/.csdp.cache
diff --git a/test-suite/Makefile b/test-suite/Makefile
index 168a662fd7..928a77cb8e 100644
--- a/test-suite/Makefile
+++ b/test-suite/Makefile
@@ -250,11 +250,19 @@ $(addsuffix .log,$(wildcard bugs/closed/*.v)): %.v.log: %.v
 # Unit tests
 #######################################################################
 
+# An alternative is ifeq ($(OS),Windows_NT) using make's own variable.
+ifeq ($(ARCH),win32)
+  export FINDLIB_SEP=";"
+else
+  export FINDLIB_SEP=":"
+endif
+
 # COQLIBINSTALL is quoted in config/make thus we must unquote it,
 # otherwise the directory name will include the quotes, see
 # see for example https://stackoverflow.com/questions/10424645/how-to-convert-a-quoted-string-to-a-normal-one-in-makefile
+
 ifeq ($(LOCAL),true)
-  export OCAMLPATH := $(shell echo $(COQLIBINSTALL):$$OCAMLPATH)
+  export OCAMLPATH := $(shell echo $(COQLIBINSTALL)$(FINDLIB_SEP)$$OCAMLPATH)
 endif
 
 OCAMLOPT := $(OCAMLFIND) opt $(CAMLFLAGS)
diff --git a/test-suite/bugs/closed/bug_3690.v b/test-suite/bugs/closed/bug_3690.v
index fa30132ab5..9273a20e19 100644
--- a/test-suite/bugs/closed/bug_3690.v
+++ b/test-suite/bugs/closed/bug_3690.v
@@ -41,8 +41,5 @@ Type@{Top.34} -> Type@{Top.37}
                                   Top.36 < Top.34
                                   Top.37 < Top.36
                                    *) *)
-Fail Check @qux@{Set Set}.
-Check @qux@{Type Type Type Type}.
-(* [qux] should only need two universes *)
-Check @qux@{i j k l}.  (* Error: The command has not failed!, but I think this is suboptimal *)
-Fail Check @qux@{i j}.
+Check @qux@{Type Type}.
+(* used to have 4 universes *)
diff --git a/test-suite/bugs/closed/bug_3956.v b/test-suite/bugs/closed/bug_3956.v
index 115284ec02..456fa11bd0 100644
--- a/test-suite/bugs/closed/bug_3956.v
+++ b/test-suite/bugs/closed/bug_3956.v
@@ -129,13 +129,13 @@ Module Comodality_Theory (F : Comodality).
       := IdmapM FPM.
     Module cip_FPM := FPM.coindpathsM FPM cmpinv_o_cmp_M idmap_FPM.
     Module cip_FPHM <: HomotopyM FPM cmpM.PM cip_FPM.fhM cip_FPM.fkM.
-      Definition m : forall x, cip_FPM.fhM.m@{i j} x = cip_FPM.fkM.m@{i j} x.
+      Definition m : forall x, cip_FPM.fhM.m x = cip_FPM.fkM.m x.
       Proof.
         intros x.
-        refine (concat (cmpinvM.m_beta@{i j} (cmpM.m@{i j} x)) _).
+        refine (concat (cmpinvM.m_beta (cmpM.m x)) _).
         apply path_prod@{i i i}; simpl.
-        - exact (cmpM.FfstM.mM.m_beta@{i j} x).
-        - exact (cmpM.FsndM.mM.m_beta@{i j} x).
+        - exact (cmpM.FfstM.mM.m_beta x).
+        - exact (cmpM.FsndM.mM.m_beta x).
       Defined.
     End cip_FPHM.
   End isequiv_F_prod_cmp_M.
diff --git a/test-suite/bugs/closed/bug_4132.v b/test-suite/bugs/closed/bug_4132.v
index 806ffb771f..67ecc3087f 100644
--- a/test-suite/bugs/closed/bug_4132.v
+++ b/test-suite/bugs/closed/bug_4132.v
@@ -26,6 +26,6 @@ Qed.
 
 Lemma foo3 x y (b := 0) (H1 : x <= y) (H2 : y <= b) : x <= b.
 omega. (* Pierre L: according to a comment of bug report #4132,
-          this might have triggered "Failure(occurence 2)" in the past,
+          this might have triggered "Failure(occurrence 2)" in the past,
           but I never managed to reproduce that. *)
 Qed.
diff --git a/test-suite/bugs/closed/bug_7631.v b/test-suite/bugs/closed/bug_7631.v
index 34eb8b8676..93aeb83e28 100644
--- a/test-suite/bugs/closed/bug_7631.v
+++ b/test-suite/bugs/closed/bug_7631.v
@@ -7,6 +7,7 @@ Section Foo.
 Let bar := foo.
 
 Eval native_compute in bar.
+Eval vm_compute in bar.
 
 End Foo.
 
@@ -17,5 +18,6 @@ Module RelContext.
 Definition foo := true.
 
 Definition bar (x := foo) := Eval native_compute in x.
+Definition barvm (x := foo) := Eval vm_compute in x.
 
 End RelContext.
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.
diff --git a/test-suite/success/btauto.v b/test-suite/success/btauto.v
new file mode 100644
index 0000000000..d2512b5cbb
--- /dev/null
+++ b/test-suite/success/btauto.v
@@ -0,0 +1,9 @@
+Require Import Btauto.
+
+Open Scope bool_scope.
+
+Lemma test_orb a b : (if a || b then negb (negb b && negb a) else negb a && negb b) = true.
+Proof. btauto. Qed.
+
+Lemma test_xorb a : xorb a a = false.
+Proof. btauto. Qed.
diff --git a/test-suite/success/univers.v b/test-suite/success/univers.v
index 2863404590..28426b5700 100644
--- a/test-suite/success/univers.v
+++ b/test-suite/success/univers.v
@@ -60,7 +60,7 @@ Qed.
 
 Record U : Type := { A:=Type; a:A }.
 
-(** Check assignement of sorts to inductives and records. *)
+(** Check assignment of sorts to inductives and records. *)
 
 Variable sh : list nat.