12 files changed, 32 insertions, 12 deletions
diff --git a/test-suite/coq-makefile/coqdoc1/run.sh b/test-suite/coq-makefile/coqdoc1/run.sh
index 0d9b9ea867..88237815b1 100755
--- a/test-suite/coq-makefile/coqdoc1/run.sh
+++ b/test-suite/coq-makefile/coqdoc1/run.sh
@@ -28,12 +28,10 @@ sort -u > desired <<EOT
 ./test/test.glob
 ./test/test.v
 ./test/test.vo
-./test/test.vos
 ./test/sub
 ./test/sub/testsub.glob
 ./test/sub/testsub.v
 ./test/sub/testsub.vo
-./test/sub/testsub.vos
 ./test/mlihtml
 ./test/mlihtml/index_exceptions.html
 ./test/mlihtml/index.html
diff --git a/test-suite/coq-makefile/coqdoc2/run.sh b/test-suite/coq-makefile/coqdoc2/run.sh
index 852ac372f4..5811dd17e4 100755
--- a/test-suite/coq-makefile/coqdoc2/run.sh
+++ b/test-suite/coq-makefile/coqdoc2/run.sh
@@ -26,12 +26,10 @@ sort -u > desired <<EOT
 ./test/test.glob
 ./test/test.v
 ./test/test.vo
-./test/test.vos
 ./test/sub
 ./test/sub/testsub.glob
 ./test/sub/testsub.v
 ./test/sub/testsub.vo
-./test/sub/testsub.vos
 ./test/mlihtml
 ./test/mlihtml/index_exceptions.html
 ./test/mlihtml/index.html
diff --git a/test-suite/coq-makefile/mlpack1/run.sh b/test-suite/coq-makefile/mlpack1/run.sh
index 1303aa90b6..bbd2fc460c 100755
--- a/test-suite/coq-makefile/mlpack1/run.sh
+++ b/test-suite/coq-makefile/mlpack1/run.sh
@@ -19,6 +19,5 @@ sort > desired <<EOT
 ./test/test_plugin.cmxs
 ./test/test.v
 ./test/test.vo
-./test/test.vos
 EOT
 exec diff -u desired actual
diff --git a/test-suite/coq-makefile/mlpack2/run.sh b/test-suite/coq-makefile/mlpack2/run.sh
index 1303aa90b6..bbd2fc460c 100755
--- a/test-suite/coq-makefile/mlpack2/run.sh
+++ b/test-suite/coq-makefile/mlpack2/run.sh
@@ -19,6 +19,5 @@ sort > desired <<EOT
 ./test/test_plugin.cmxs
 ./test/test.v
 ./test/test.vo
-./test/test.vos
 EOT
 exec diff -u desired actual
diff --git a/test-suite/coq-makefile/multiroot/run.sh b/test-suite/coq-makefile/multiroot/run.sh
index 3a5425c8bf..45bf1481df 100755
--- a/test-suite/coq-makefile/multiroot/run.sh
+++ b/test-suite/coq-makefile/multiroot/run.sh
@@ -29,12 +29,10 @@ sort > desired <<EOT
 ./test/test_plugin.cmxs
 ./test/test.v
 ./test/test.vo
-./test/test.vos
 ./test2
 ./test2/test.glob
 ./test2/test.v
 ./test2/test.vo
-./test2/test.vos
 ./orphan_test_test2_test
 ./orphan_test_test2_test/html
 ./orphan_test_test2_test/html/coqdoc.css
diff --git a/test-suite/coq-makefile/native1/run.sh b/test-suite/coq-makefile/native1/run.sh
index 588de82613..8f9ab9a711 100755
--- a/test-suite/coq-makefile/native1/run.sh
+++ b/test-suite/coq-makefile/native1/run.sh
@@ -22,7 +22,6 @@ sort > desired <<EOT
 ./test/test_plugin.cmxs
 ./test/test.v
 ./test/test.vo
-./test/test.vos
 ./test/.coq-native
 ./test/.coq-native/Ntest_test.cmi
 ./test/.coq-native/Ntest_test.cmx
diff --git a/test-suite/coq-makefile/plugin1/run.sh b/test-suite/coq-makefile/plugin1/run.sh
index cd47187582..1e2bd979b3 100755
--- a/test-suite/coq-makefile/plugin1/run.sh
+++ b/test-suite/coq-makefile/plugin1/run.sh
@@ -22,6 +22,5 @@ sort > desired <<EOT
 ./test/test_plugin.cmxs
 ./test/test.v
 ./test/test.vo
-./test/test.vos
 EOT
 exec diff -u desired actual
diff --git a/test-suite/coq-makefile/plugin2/run.sh b/test-suite/coq-makefile/plugin2/run.sh
index cd47187582..1e2bd979b3 100755
--- a/test-suite/coq-makefile/plugin2/run.sh
+++ b/test-suite/coq-makefile/plugin2/run.sh
@@ -22,6 +22,5 @@ sort > desired <<EOT
 ./test/test_plugin.cmxs
 ./test/test.v
 ./test/test.vo
-./test/test.vos
 EOT
 exec diff -u desired actual
diff --git a/test-suite/coq-makefile/plugin3/run.sh b/test-suite/coq-makefile/plugin3/run.sh
index cd47187582..1e2bd979b3 100755
--- a/test-suite/coq-makefile/plugin3/run.sh
+++ b/test-suite/coq-makefile/plugin3/run.sh
@@ -22,6 +22,5 @@ sort > desired <<EOT
 ./test/test_plugin.cmxs
 ./test/test.v
 ./test/test.vo
-./test/test.vos
 EOT
 exec diff -u desired actual
diff --git a/test-suite/output/Notations4.out b/test-suite/output/Notations4.out
index c1b9a2b1c6..ba4ac5a8f9 100644
--- a/test-suite/output/Notations4.out
+++ b/test-suite/output/Notations4.out
@@ -57,3 +57,5 @@ where
      |- Type] (pat, p0, p cannot be used)
 ?T0 : [y : nat  pat : ?T0 * nat  p0 : ?T0 * nat  p := p0 : ?T0 * nat
       |- Type] (pat, p0, p cannot be used)
+fun '{| |} => true
+     : R -> bool
diff --git a/test-suite/output/Notations4.v b/test-suite/output/Notations4.v
index d1063bfd04..4b9d0abd95 100644
--- a/test-suite/output/Notations4.v
+++ b/test-suite/output/Notations4.v
@@ -133,3 +133,10 @@ Check fun y : nat => # (x,z) |-> y & y.
 Check fun y : nat => # (x,z) |-> (x + y) & (y + z).
 
 End K.
+
+Module EmptyRecordSyntax.
+
+Record R := { n : nat }.
+Check fun '{|n:=x|} => true.
+
+End EmptyRecordSyntax.
diff --git a/test-suite/success/RefineInstance.v b/test-suite/success/RefineInstance.v
new file mode 100644
index 0000000000..f4d2f07db5
--- /dev/null
+++ b/test-suite/success/RefineInstance.v
@@ -0,0 +1,23 @@
+
+
+Class Foo := foo { a : nat; b : bool }.
+
+Fail Instance bla : Foo := { b:= true }.
+
+#[refine] Instance bla : Foo := { b:= true }.
+Proof.
+exact 0.
+Defined.
+
+Instance bli : Foo := { a:=1; b := false}.
+Check bli.
+
+Fail #[program, refine] Instance bla : Foo := {b := true}.
+
+#[program] Instance blo : Foo := {b := true}.
+Next Obligation. exact 2. Qed.
+Check blo.
+
+#[refine] Instance xbar : Foo := {a:=4; b:=true}.
+Proof. Qed.
+Check xbar.