From f41968d8c240db4653d0b9fe76e1646cd7c6fb68 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Thu, 3 Dec 2015 19:08:51 +0100
Subject: Univs: fix bug #4443.

Do not substitute rigid variables during minimization, keeping
their equality constraints instead.
---
 test-suite/bugs/closed/4443.v | 31 +++++++++++++++++++++++++++++++
 1 file changed, 31 insertions(+)
 create mode 100644 test-suite/bugs/closed/4443.v

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/4443.v b/test-suite/bugs/closed/4443.v
new file mode 100644
index 0000000000..66dfa0e685
--- /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
-- 
cgit v1.2.3


From 387351b4c0ffeff65d8a7192f5073cfd4bd20f53 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 5 Dec 2015 00:14:37 +0100
Subject: Changing "destruct !hyp" into "destruct (hyp)" (and similarly for
 induction) based on a suggestion of Guillaume M. (done like this in
 ssreflect).

This is actually consistent with the hack of using "destruct (1)" to
mean the term 1 by opposition to the use of "destruct 1" to mean the
first non-dependent hypothesis of the goal.
---
 test-suite/success/destruct.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'test-suite')

diff --git a/test-suite/success/destruct.v b/test-suite/success/destruct.v
index 59cd25cd76..9f091e3996 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.
 
-- 
cgit v1.2.3


From df3a49a18c5b01984000df9244ecea9c275b30cd Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Mon, 7 Dec 2015 10:52:14 +0100
Subject: Fix some typos.

---
 test-suite/Makefile | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'test-suite')

diff --git a/test-suite/Makefile b/test-suite/Makefile
index 7150d1fd4f..207f25ed0b 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 $<
-- 
cgit v1.2.3