Univs: add Strict Universe Declaration option (on by default)

This option disallows "declare at first use" semantics for universe
variables (in @{}), forcing the declaration of _all_ universes appearing
in a definition when introducing it with syntax Definition/Inductive
foo@{i j k} .. The bound universes at the end of a definition/inductive
must be exactly those ones, no extras allowed currently.
Test-suite files using the old semantics just disable the option.

22 files changed, 33 insertions, 0 deletions

diff --git a/test-suite/bugs/closed/3330.v b/test-suite/bugs/closed/3330.v
index 4cd7c39e88..e6a50449da 100644
--- a/test-suite/bugs/closed/3330.v
+++ b/test-suite/bugs/closed/3330.v
@@ -1,3 +1,4 @@
+Unset Strict Universe Declaration.
 Require Import TestSuite.admit.
 (* File reduced by coq-bug-finder from original input, then from 12106 lines to 1070 lines *)
 Set Universe Polymorphism.
diff --git a/test-suite/bugs/closed/3352.v b/test-suite/bugs/closed/3352.v
index b57b0a0f0b..f8113e4c78 100644
--- a/test-suite/bugs/closed/3352.v
+++ b/test-suite/bugs/closed/3352.v
@@ -1,3 +1,4 @@
+Unset Strict Universe Declaration.
 
 (*
 I'm not sure what the general rule should be; intuitively, I want [IsHProp (* Set *) Foo] to mean [IsHProp (* U >= Set *) Foo].  (I think this worked in HoTT/coq, too.)  Morally, [IsHProp] has no universe level associated with it distinct from that of its argument, you should never get a universe inconsistency from unifying [IsHProp A] with [IsHProp A].  (The issue is tricker when IsHProp uses [A] elsewhere, as in:
diff --git a/test-suite/bugs/closed/3386.v b/test-suite/bugs/closed/3386.v
index 0e236c2172..b8bb8bce09 100644
--- a/test-suite/bugs/closed/3386.v
+++ b/test-suite/bugs/closed/3386.v
@@ -1,3 +1,4 @@
+Unset Strict Universe Declaration.
 Set Universe Polymorphism.
 Set Printing Universes.
 Record Cat := { Obj :> Type }.
diff --git a/test-suite/bugs/closed/3387.v b/test-suite/bugs/closed/3387.v
index ae212caa5d..cb435e7865 100644
--- a/test-suite/bugs/closed/3387.v
+++ b/test-suite/bugs/closed/3387.v
@@ -1,3 +1,4 @@
+Unset Strict Universe Declaration.
 Set Universe Polymorphism.
 Set Printing Universes.
 Record Cat := { Obj :> Type }.
diff --git a/test-suite/bugs/closed/3559.v b/test-suite/bugs/closed/3559.v
index 50645090fa..da12b68689 100644
--- a/test-suite/bugs/closed/3559.v
+++ b/test-suite/bugs/closed/3559.v
@@ -1,3 +1,4 @@
+Unset Strict Universe Declaration.
 (* File reduced by coq-bug-finder from original input, then from 8657 lines to
 4731 lines, then from 4174 lines to 192 lines, then from 161 lines to 55 lines,
 then from 51 lines to 37 lines, then from 43 lines to 30 lines *)
diff --git a/test-suite/bugs/closed/3566.v b/test-suite/bugs/closed/3566.v
index b2aa8c3cd6..e2d7976981 100644
--- a/test-suite/bugs/closed/3566.v
+++ b/test-suite/bugs/closed/3566.v
@@ -1,3 +1,4 @@
+Unset Strict Universe Declaration.
 Notation idmap := (fun x => x).
 Inductive paths {A : Type} (a : A) : A -> Type := idpath : paths a a.
 Arguments idpath {A a} , [A] a.
diff --git a/test-suite/bugs/closed/3666.v b/test-suite/bugs/closed/3666.v
index a5b0e9347d..e69ec10976 100644
--- a/test-suite/bugs/closed/3666.v
+++ b/test-suite/bugs/closed/3666.v
@@ -1,3 +1,4 @@
+Unset Strict Universe Declaration.
 (* File reduced by coq-bug-finder from original input, then from 11542 lines to 325 lines, then from 347 lines to 56 lines, then from 58 lines to 15 lines *)
 (* coqc version trunk (September 2014) compiled on Sep 25 2014 2:53:46 with OCaml 4.01.0
    coqtop version cagnode16:/afs/csail.mit.edu/u/j/jgross/coq-trunk,trunk (bec7e0914f4a7144cd4efa8ffaccc9f72dbdb790) *)
diff --git a/test-suite/bugs/closed/3690.v b/test-suite/bugs/closed/3690.v
index 4069e38075..df9f5f4761 100644
--- a/test-suite/bugs/closed/3690.v
+++ b/test-suite/bugs/closed/3690.v
@@ -1,3 +1,4 @@
+Unset Strict Universe Declaration.
 Set Printing Universes.
 Set Universe Polymorphism.
 Definition foo (a := Type) (b := Type) (c := Type) := Type.
diff --git a/test-suite/bugs/closed/3777.v b/test-suite/bugs/closed/3777.v
index b9b2dd6b3e..e203528fcc 100644
--- a/test-suite/bugs/closed/3777.v
+++ b/test-suite/bugs/closed/3777.v
@@ -1,3 +1,4 @@
+Unset Strict Universe Declaration.
 Module WithoutPoly.
   Unset Universe Polymorphism.
   Definition foo (A : Type@{i}) (B : Type@{i}) := A -> B.
diff --git a/test-suite/bugs/closed/3779.v b/test-suite/bugs/closed/3779.v
index eb0d206c5c..2b44e225e8 100644
--- a/test-suite/bugs/closed/3779.v
+++ b/test-suite/bugs/closed/3779.v
@@ -1,3 +1,4 @@
+Unset Strict Universe Declaration.
 Set Universe Polymorphism.
 Record UnitSubuniverse := { a : Type@{sm} ; x : (Type@{sm} : Type@{lg}) ; inO_internal : Type@{lg} -> Type@{lg} }.
 Class In (O : UnitSubuniverse@{sm lg}) (T : Type@{lg}) := in_inO_internal : inO_internal O T.
diff --git a/test-suite/bugs/closed/3808.v b/test-suite/bugs/closed/3808.v
index 6e19ddf8dc..a5c84e6856 100644
--- a/test-suite/bugs/closed/3808.v
+++ b/test-suite/bugs/closed/3808.v
@@ -1,2 +1,3 @@
+Unset Strict Universe Declaration.
 Inductive Foo : (let enforce := (fun x => x) : Type@{j} -> Type@{i} in Type@{i})
   := foo : Foo.
\ No newline at end of file
diff --git a/test-suite/bugs/closed/3821.v b/test-suite/bugs/closed/3821.v
index 8da4f73626..30261ed266 100644
--- a/test-suite/bugs/closed/3821.v
+++ b/test-suite/bugs/closed/3821.v
@@ -1,2 +1,3 @@
+Unset Strict Universe Declaration.
 Inductive quotient {A : Type@{i}} {B : Type@{j}} : Type@{max(i, j)} := .
 
diff --git a/test-suite/bugs/closed/3922.v b/test-suite/bugs/closed/3922.v
index 0ccc92067d..5013bc6ac1 100644
--- a/test-suite/bugs/closed/3922.v
+++ b/test-suite/bugs/closed/3922.v
@@ -1,3 +1,4 @@
+Unset Strict Universe Declaration.
 Require Import TestSuite.admit.
 Set Universe Polymorphism.
 Notation Type0 := Set.
diff --git a/test-suite/bugs/closed/4089.v b/test-suite/bugs/closed/4089.v
index c6cb9c35e6..e4d76732a3 100644
--- a/test-suite/bugs/closed/4089.v
+++ b/test-suite/bugs/closed/4089.v
@@ -1,3 +1,4 @@
+Unset Strict Universe Declaration.
 Require Import TestSuite.admit.
 (* -*- mode: coq; coq-prog-args: ("-emacs" "-indices-matter") -*- *)
 (* File reduced by coq-bug-finder from original input, then from 6522 lines to 318 lines, then from 1139 lines to 361 lines *)
diff --git a/test-suite/bugs/closed/4121.v b/test-suite/bugs/closed/4121.v
index 5f8c411ca8..d34a2b8b1b 100644
--- a/test-suite/bugs/closed/4121.v
+++ b/test-suite/bugs/closed/4121.v
@@ -1,3 +1,4 @@
+Unset Strict Universe Declaration.
 (* -*- coq-prog-args: ("-emacs" "-nois") -*- *)
 (* File reduced by coq-bug-finder from original input, then from 830 lines to 47 lines, then from 25 lines to 11 lines *)
 (* coqc version 8.5beta1 (March 2015) compiled on Mar 11 2015 18:51:36 with OCaml 4.01.0
diff --git a/test-suite/bugs/closed/4287.v b/test-suite/bugs/closed/4287.v
index e139c5b6c9..0623cf5b84 100644
--- a/test-suite/bugs/closed/4287.v
+++ b/test-suite/bugs/closed/4287.v
@@ -1,3 +1,4 @@
+Unset Strict Universe Declaration.
 
 Universe b.
 
diff --git a/test-suite/bugs/closed/4299.v b/test-suite/bugs/closed/4299.v
new file mode 100644
index 0000000000..955c3017d7
--- /dev/null
+++ b/test-suite/bugs/closed/4299.v
@@ -0,0 +1,12 @@
+Unset Strict Universe Declaration.
+Set Universe Polymorphism.
+
+Module Type Foo.
+  Definition U := Type : Type.
+  Parameter eq : Type = U.
+End Foo.
+
+Module M : Foo with Definition U := Type : Type.
+  Definition U := let X := Type in Type.
+  Definition eq : Type = U := eq_refl.
+Fail End M.
\ No newline at end of file
diff --git a/test-suite/bugs/closed/4301.v b/test-suite/bugs/closed/4301.v
index 3b00efb213..b4e17c2231 100644
--- a/test-suite/bugs/closed/4301.v
+++ b/test-suite/bugs/closed/4301.v
@@ -1,3 +1,4 @@
+Unset Strict Universe Declaration.
 Set Universe Polymorphism.
 
 Module Type Foo.
diff --git a/test-suite/bugs/closed/HoTT_coq_007.v b/test-suite/bugs/closed/HoTT_coq_007.v
index 0b8bb23534..844ff87566 100644
--- a/test-suite/bugs/closed/HoTT_coq_007.v
+++ b/test-suite/bugs/closed/HoTT_coq_007.v
@@ -1,3 +1,4 @@
+Unset Strict Universe Declaration.
 Require Import TestSuite.admit.
 Module Comment1.
   Set Implicit Arguments.
diff --git a/test-suite/bugs/closed/HoTT_coq_036.v b/test-suite/bugs/closed/HoTT_coq_036.v
index 4c3e078a50..7a84531a77 100644
--- a/test-suite/bugs/closed/HoTT_coq_036.v
+++ b/test-suite/bugs/closed/HoTT_coq_036.v
@@ -1,3 +1,4 @@
+Unset Strict Universe Declaration.
 Module Version1.
   Set Implicit Arguments.
   Set Universe Polymorphism.
diff --git a/test-suite/bugs/closed/HoTT_coq_062.v b/test-suite/bugs/closed/HoTT_coq_062.v
index b7db22a69e..90d1d18306 100644
--- a/test-suite/bugs/closed/HoTT_coq_062.v
+++ b/test-suite/bugs/closed/HoTT_coq_062.v
@@ -1,3 +1,4 @@
+Unset Strict Universe Declaration.
 Require Import TestSuite.admit.
 (* -*- mode: coq; coq-prog-args: ("-emacs" "-indices-matter") -*- *)
 (* File reduced by coq-bug-finder from 5012 lines to 4659 lines, then from 4220 lines to 501 lines, then from 513 lines to 495 lines, then from 513 lines to 495 lines, then from 412 lines to 79 lines, then from 412 lines to 79 lines. *)
diff --git a/test-suite/bugs/closed/HoTT_coq_093.v b/test-suite/bugs/closed/HoTT_coq_093.v
index f382dac976..4f8868d538 100644
--- a/test-suite/bugs/closed/HoTT_coq_093.v
+++ b/test-suite/bugs/closed/HoTT_coq_093.v
@@ -1,3 +1,4 @@
+Unset Strict Universe Declaration.
 (** It would be nice if we had more lax constraint checking of inductive types, and had variance annotations on their universes *)
 Set Printing All.
 Set Printing Implicit.