Merge branch 'v8.5'

3 files changed, 33 insertions, 2 deletions

diff --git a/test-suite/Makefile b/test-suite/Makefile
index 742395422..f333ae63e 100644
--- a/test-suite/Makefile
+++ b/test-suite/Makefile
@@ -352,7 +352,7 @@ $(addsuffix .log,$(wildcard ideal-features/*.v)): %.v.log: %.v
           fi; \
 	} > "$@"
 
-# Additionnal dependencies for module tests
+# Additional dependencies for module tests
 $(addsuffix .log,$(wildcard modules/*.v)): %.v.log: modules/Nat.vo modules/plik.vo
 modules/%.vo: modules/%.v
 	$(HIDE)$(coqtop) -R modules Mods -compile $<
diff --git a/test-suite/bugs/closed/4443.v b/test-suite/bugs/closed/4443.v
new file mode 100644
index 000000000..66dfa0e68
--- /dev/null
+++ b/test-suite/bugs/closed/4443.v
@@ -0,0 +1,31 @@
+Set Universe Polymorphism.
+
+Record TYPE@{i} := cType {
+  type : Type@{i};
+}.
+
+Definition PROD@{i j k}
+  (A : Type@{i})
+  (B : A -> Type@{j})
+  : TYPE@{k}.
+Proof.
+  refine (cType@{i} _).
++ refine (forall x : A, B x).
+Defined.
+
+Local Unset Strict Universe Declaration.
+Definition PRODinj
+  (A : Type@{i})
+  (B : A -> Type)
+  : TYPE.
+Proof.
+  refine (cType@{i} _).
++ refine (forall x : A, B x).
+Defined.
+
+  Monomorphic Universe i j.
+  Monomorphic Constraint j < i.
+Set Printing Universes.
+Check PROD@{i i i}.
+Check PRODinj@{i j}.
+Fail Check PRODinj@{j i}.
\ No newline at end of file
diff --git a/test-suite/success/destruct.v b/test-suite/success/destruct.v
index 59cd25cd7..9f091e399 100644
--- a/test-suite/success/destruct.v
+++ b/test-suite/success/destruct.v
@@ -389,7 +389,7 @@ Abort.
 
 Goal forall b:bool, True.
 intro b.
-destruct !b.
+destruct (b).
 clear b. (* b has to be here *)
 Abort.