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.

26 files changed, 64 insertions, 0 deletions

diff --git a/test-suite/bugs/closed/3330.v b/test-suite/bugs/closed/3330.v
index 4cd7c39e8..e6a50449d 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 b57b0a0f0..f8113e4c7 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 0e236c217..b8bb8bce0 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 ae212caa5..cb435e786 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 50645090f..da12b6868 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 b2aa8c3cd..e2d797698 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 a5b0e9347..e69ec1097 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 4069e3807..df9f5f476 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 b9b2dd6b3..e203528fc 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 eb0d206c5..2b44e225e 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 6e19ddf8d..a5c84e685 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 8da4f7362..30261ed26 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 0ccc92067..5013bc6ac 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 c6cb9c35e..e4d76732a 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 5f8c411ca..d34a2b8b1 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 e139c5b6c..0623cf5b8 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 000000000..955c3017d
--- /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 3b00efb21..b4e17c223 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 0b8bb2353..844ff8756 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 4c3e078a5..7a84531a7 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 b7db22a69..90d1d1830 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 f382dac97..4f8868d53 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.
diff --git a/test-suite/bugs/opened/3754.v b/test-suite/bugs/opened/3754.v
index 9b3f94d91..a717bbe73 100644
--- a/test-suite/bugs/opened/3754.v
+++ b/test-suite/bugs/opened/3754.v
@@ -1,3 +1,4 @@
+Unset Strict Universe Declaration.
 Require Import TestSuite.admit.
 (* File reduced by coq-bug-finder from original input, then from 9113 lines to 279 lines *)
 (* coqc version trunk (October 2014) compiled on Oct 19 2014 18:56:9 with OCaml 3.12.1
diff --git a/test-suite/success/namedunivs.v b/test-suite/success/namedunivs.v
index 059462fac..f9154ef57 100644
--- a/test-suite/success/namedunivs.v
+++ b/test-suite/success/namedunivs.v
@@ -4,6 +4,8 @@
 (* Fail  exact H. *)
 (* Section . *)
 
+Unset Strict Universe Declaration.
+
 Section lift_strict.
 Polymorphic Definition liftlt := 
   let t := Type@{i} : Type@{k} in
diff --git a/test-suite/success/polymorphism.v b/test-suite/success/polymorphism.v
index 957612ef1..d6bbfe29a 100644
--- a/test-suite/success/polymorphism.v
+++ b/test-suite/success/polymorphism.v
@@ -1,3 +1,5 @@
+Unset Strict Universe Declaration.
+
 Module withoutpoly.
 
 Inductive empty :=. 
diff --git a/test-suite/success/univnames.v b/test-suite/success/univnames.v
new file mode 100644
index 000000000..31d264f64
--- /dev/null
+++ b/test-suite/success/univnames.v
@@ -0,0 +1,26 @@
+Set Universe Polymorphism.
+
+Definition foo@{i j} (A : Type@{i}) (B : Type@{j}) := A.
+
+Set Printing Universes.
+
+Fail Definition bar@{i} (A : Type@{i}) (B : Type) := A.
+
+Definition baz@{i j} (A : Type@{i}) (B : Type@{j}) := (A * B)%type.
+
+Fail Definition bad@{i j} (A : Type@{i}) (B : Type@{j}) : Type := (A * B)%type.
+
+Fail Definition bad@{i} (A : Type@{i}) (B : Type@{j}) : Type := (A * B)%type.
+
+Definition shuffle@{i j} (A : Type@{j}) (B : Type@{i}) := (A * B)%type.
+
+Definition nothing (A : Type) := A.
+
+Inductive bla@{l k} : Type@{k} := blaI : Type@{l} -> bla.
+
+Inductive blacopy@{k l} : Type@{k} := blacopyI : Type@{l} -> blacopy.
+
+
+Universe g.
+
+Inductive blacopy'@{l} : Type@{g} := blacopy'I : Type@{l} -> blacopy'.
\ No newline at end of file