From 60770e86f4ec925fce52ad3565a92beb98d253c1 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Fri, 15 Sep 2017 22:21:46 +0200
Subject: Stop exposing UState.universe_context and its Evd wrapper.

We can enforce properties through check_univ_decl, or get an arbitrary
ordered context with UState.context / Evd.to_universe_context (the
later being a new wrapper of the former).
---
 test-suite/success/polymorphism.v | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'test-suite')

diff --git a/test-suite/success/polymorphism.v b/test-suite/success/polymorphism.v
index 7eaafc3545..00cab744eb 100644
--- a/test-suite/success/polymorphism.v
+++ b/test-suite/success/polymorphism.v
@@ -190,6 +190,8 @@ Module binders.
     Fail Defined.
   Abort.
 
+  Fail Lemma bar@{u v | } : let x := (fun x => x) : Type@{u} -> Type@{v} in nat.
+
   Lemma bar@{i j| i < j} : Type@{j}.
   Proof.
     exact Type@{i}.
-- 
cgit v1.2.3


From 4eb6d29d1ca7e0cc28d59d19a50adb83f7b30a2a Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Fri, 15 Sep 2017 23:39:11 +0200
Subject: Fix defining non primitive projections with abstracted universes.

I think this only affects printing (in the new test you would get
[Var (0)] when printing runwrap) but is still ugly.
---
 test-suite/output/UnivBinders.out | 51 ++++++++++++++++++++++++++++++++++++---
 test-suite/output/UnivBinders.v   | 26 ++++++++++++++++++--
 2 files changed, 71 insertions(+), 6 deletions(-)

(limited to 'test-suite')

diff --git a/test-suite/output/UnivBinders.out b/test-suite/output/UnivBinders.out
index 904ff68aa7..1bacb75134 100644
--- a/test-suite/output/UnivBinders.out
+++ b/test-suite/output/UnivBinders.out
@@ -1,12 +1,55 @@
+NonCumulative Inductive Empty@{u} : Type@{u} :=  
+NonCumulative Record PWrap (A : Type@{u}) : Type@{u} := pwrap { punwrap : A }
+
+PWrap has primitive projections with eta conversion.
+For PWrap: Argument scope is [type_scope]
+For pwrap: Argument scopes are [type_scope _]
+punwrap@{u} = 
+fun (A : Type@{u}) (p : PWrap@{u} A) => punwrap _ p
+     : forall A : Type@{u}, PWrap@{u} A -> A
+(* u |=  *)
+
+punwrap is universe polymorphic
+Argument scopes are [type_scope _]
+NonCumulative Record RWrap (A : Type@{u}) : Type@{u} := rwrap { runwrap : A }
+
+For RWrap: Argument scope is [type_scope]
+For rwrap: Argument scopes are [type_scope _]
+runwrap@{u} = 
+fun (A : Type@{u}) (r : RWrap@{u} A) => let (runwrap) := r in runwrap
+     : forall A : Type@{u}, RWrap@{u} A -> A
+(* u |=  *)
+
+runwrap is universe polymorphic
+Argument scopes are [type_scope _]
+Wrap@{u} = fun A : Type@{u} => A
+     : Type@{u} -> Type@{u}
+(* u |=  *)
+
+Wrap is universe polymorphic
+Argument scope is [type_scope]
+wrap@{u} = 
+fun (A : Type@{u}) (Wrap : Wrap@{u} A) => Wrap
+     : forall A : Type@{u}, Wrap@{u} A -> A
+(* u |=  *)
+
+wrap is universe polymorphic
+Arguments A, Wrap are implicit and maximally inserted
+Argument scopes are [type_scope _]
 bar@{u} = nat
      : Wrap@{u} Set
 (* u |= Set < u
          *)
 
 bar is universe polymorphic
-foo@{u Top.8 v} = 
-Type@{Top.8} -> Type@{v} -> Type@{u}
-     : Type@{max(u+1, Top.8+1, v+1)}
-(* u Top.8 v |=  *)
+foo@{u Top.17 v} = 
+Type@{Top.17} -> Type@{v} -> Type@{u}
+     : Type@{max(u+1, Top.17+1, v+1)}
+(* u Top.17 v |=  *)
 
 foo is universe polymorphic
+Monomorphic mono = Type@{u}
+     : Type@{u+1}
+(* u |=  *)
+
+mono is not universe polymorphic
diff --git a/test-suite/output/UnivBinders.v b/test-suite/output/UnivBinders.v
index 8656ff1a39..2c378e795d 100644
--- a/test-suite/output/UnivBinders.v
+++ b/test-suite/output/UnivBinders.v
@@ -2,12 +2,34 @@ Set Universe Polymorphism.
 Set Printing Universes.
 Unset Strict Universe Declaration.
 
-Class Wrap A := wrap : A.
+(* universe binders on inductive types and record projections *)
+Inductive Empty@{u} : Type@{u} := .
+Print Empty.
 
-Instance bar@{u} : Wrap@{u} Set. Proof nat.
+Set Primitive Projections.
+Record PWrap@{u} (A:Type@{u}) := pwrap { punwrap : A }.
+Print PWrap.
+Print punwrap.
+
+Unset Primitive Projections.
+Record RWrap@{u} (A:Type@{u}) := rwrap { runwrap : A }.
+Print RWrap.
+Print runwrap.
+
+(* universe binders also go on the constants for operational typeclasses. *)
+Class Wrap@{u} (A:Type@{u}) := wrap : A.
+Print Wrap.
+Print wrap.
+
+(* Instance in lemma mode used to ignore the binders. *)
+Instance bar@{u} : Wrap@{u} Set. Proof. exact nat. Qed.
 Print bar.
 
 (* The universes in the binder come first, then the extra universes in
    order of appearance. *)
 Definition foo@{u +} := Type -> Type@{v} -> Type@{u}.
 Print foo.
+
+(* Binders even work with monomorphic definitions! *)
+Monomorphic Definition mono@{u} := Type@{u}.
+Print mono.
-- 
cgit v1.2.3


From 02e6d7f39e3dc2aa8859274bc69b2edf8cc91feb Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Sat, 16 Sep 2017 14:05:52 +0200
Subject: restrict_universe_context: do not prune named universes.

---
 test-suite/success/polymorphism.v | 13 +++++++++++++
 1 file changed, 13 insertions(+)

(limited to 'test-suite')

diff --git a/test-suite/success/polymorphism.v b/test-suite/success/polymorphism.v
index 00cab744eb..930c165178 100644
--- a/test-suite/success/polymorphism.v
+++ b/test-suite/success/polymorphism.v
@@ -401,6 +401,19 @@ Module Anonymous.
 
 End Anonymous.
 
+Module Restrict.
+  (* Universes which don't appear in the term should be pruned, unless they have names *)
+  Set Universe Polymorphism.
+
+  Definition dummy_pruned@{} : nat := ltac:(let x := constr:(Type) in exact 0).
+
+  Definition named_not_pruned@{u} : nat := 0.
+  Check named_not_pruned@{_}.
+
+  Definition named_not_pruned_nonstrict : nat := ltac:(let x := constr:(Type@{u}) in exact 0).
+  Check named_not_pruned_nonstrict@{_}.
+End Restrict.
+
 Module F.
   Context {A B : Type}.
   Definition foo : Type := B.
-- 
cgit v1.2.3


From 58c0784745f8b2ba7523f246c4611d780c9f3f70 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Mon, 18 Sep 2017 14:50:07 +0200
Subject: When declaring constants/inductives use ContextSet if monomorphic.

Also use constant_universes_entry instead of a bool flag to indicate
polymorphism in ParameterEntry.

There are a few places where we convert back to ContextSet because
check_univ_decl returns a UContext, this could be improved.
---
 test-suite/output/UnivBinders.out | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'test-suite')

diff --git a/test-suite/output/UnivBinders.out b/test-suite/output/UnivBinders.out
index 1bacb75134..42fb52a3b3 100644
--- a/test-suite/output/UnivBinders.out
+++ b/test-suite/output/UnivBinders.out
@@ -50,6 +50,6 @@ Type@{Top.17} -> Type@{v} -> Type@{u}
 foo is universe polymorphic
 Monomorphic mono = Type@{u}
      : Type@{u+1}
-(* u |=  *)
+(* {u} |=  *)
 
 mono is not universe polymorphic
-- 
cgit v1.2.3


From 00860c1b2209159fb2b6780004c8c8ea16b3cb3a Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Mon, 18 Sep 2017 20:39:08 +0200
Subject: In close_proof only check univ decls with the restricted context.

---
 test-suite/success/polymorphism.v | 14 +++++++++++++-
 1 file changed, 13 insertions(+), 1 deletion(-)

(limited to 'test-suite')

diff --git a/test-suite/success/polymorphism.v b/test-suite/success/polymorphism.v
index 930c165178..c09a60a4d7 100644
--- a/test-suite/success/polymorphism.v
+++ b/test-suite/success/polymorphism.v
@@ -405,13 +405,25 @@ Module Restrict.
   (* Universes which don't appear in the term should be pruned, unless they have names *)
   Set Universe Polymorphism.
 
-  Definition dummy_pruned@{} : nat := ltac:(let x := constr:(Type) in exact 0).
+  Ltac exact0 := let x := constr:(Type) in exact 0.
+  Definition dummy_pruned@{} : nat := ltac:(exact0).
 
   Definition named_not_pruned@{u} : nat := 0.
   Check named_not_pruned@{_}.
 
   Definition named_not_pruned_nonstrict : nat := ltac:(let x := constr:(Type@{u}) in exact 0).
   Check named_not_pruned_nonstrict@{_}.
+
+  Lemma lemma_restrict_poly@{} : nat.
+  Proof. exact0. Defined.
+
+  Unset Universe Polymorphism.
+  Lemma lemma_restrict_mono_qed@{} : nat.
+  Proof. exact0. Qed.
+
+  Lemma lemma_restrict_abstract@{} : nat.
+  Proof. abstract exact0. Qed.
+
 End Restrict.
 
 Module F.
-- 
cgit v1.2.3


From c93d5094bff73498ec8fc02837e16cc5ce9103b6 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Thu, 7 Sep 2017 16:56:34 +0200
Subject: Make restrict_universe_context stronger.

This fixes BZ#5717.

Also add a test and fix a changed test.
---
 test-suite/bugs/closed/3690.v | 75 ++++++++++++++++++++-----------------------
 test-suite/bugs/closed/5717.v |  5 +++
 2 files changed, 40 insertions(+), 40 deletions(-)
 create mode 100644 test-suite/bugs/closed/5717.v

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/3690.v b/test-suite/bugs/closed/3690.v
index fd9640b890..fa30132ab5 100644
--- a/test-suite/bugs/closed/3690.v
+++ b/test-suite/bugs/closed/3690.v
@@ -3,49 +3,44 @@ Set Printing Universes.
 Set Universe Polymorphism.
 Definition foo (a := Type) (b := Type) (c := Type) := Type.
 Print foo.
-(* foo =
-let a := Type@{Top.1} in
-let b := Type@{Top.2} in let c := Type@{Top.3} in Type@{Top.4}
-     : Type@{Top.4+1}
-(* Top.1
-   Top.2
-   Top.3
-   Top.4 |=  *) *)
-Check @foo. (* foo@{Top.5 Top.6 Top.7
-Top.8}
-     : Type@{Top.8+1}
-(* Top.5
-   Top.6
-   Top.7
-   Top.8 |=  *) *)
+(* foo@{Top.2 Top.3 Top.5 Top.6 Top.8 Top.9 Top.10} =
+let a := Type@{Top.2} in let b := Type@{Top.5} in let c := Type@{Top.8} in Type@{Top.10}
+     : Type@{Top.10+1}
+(* Top.2 Top.3 Top.5 Top.6 Top.8 Top.9 Top.10 |= Top.2 < Top.3
+                                                 Top.5 < Top.6
+                                                 Top.8 < Top.9
+                                                  *)
+ *)
+Check @foo. (* foo@{Top.11 Top.12 Top.13 Top.14 Top.15 Top.16
+Top.17}
+     : Type@{Top.17+1}
+(* Top.11 Top.12 Top.13 Top.14 Top.15 Top.16 Top.17 |= Top.11 < Top.12
+                                                       Top.13 < Top.14
+                                                       Top.15 < Top.16
+                                                        *)
+ *)
 Definition bar := ltac:(let t := eval compute in foo in exact t).
-Check @bar. (* bar@{Top.13 Top.14 Top.15
-Top.16}
-     : Type@{Top.16+1}
-(* Top.13
-   Top.14
-   Top.15
-   Top.16 |=  *) *)
-(* The following should fail, since [bar] should only need one universe. *)
-Check @bar@{i j}.
+Check @bar. (* bar@{Top.27}
+     : Type@{Top.27+1}
+(* Top.27 |=  *) *)
+
+Check @bar@{i}.
 Definition baz (a := Type) (b := Type : a) (c := Type : b) := a -> c.
 Definition qux := Eval compute in baz.
-Check @qux. (* qux@{Top.24 Top.25
-Top.26}
-     : Type@{max(Top.24+1, Top.26+1)}
-(* Top.24
-   Top.25
-   Top.26 |= Top.25 < Top.24
-              Top.26 < Top.25
-               *) *)
-Print qux. (* qux =
-Type@{Top.21} -> Type@{Top.23}
-     : Type@{max(Top.21+1, Top.23+1)}
-(* Top.21
-   Top.22
-   Top.23 |= Top.22 < Top.21
-              Top.23 < Top.22
-               *) *)
+Check @qux. (* qux@{Top.38 Top.39 Top.40
+Top.41}
+     : Type@{max(Top.38+1, Top.41+1)}
+(* Top.38 Top.39 Top.40 Top.41 |= Top.38 < Top.39
+                                  Top.40 < Top.38
+                                  Top.41 < Top.40
+                                   *) *)
+Print qux. (* qux@{Top.34 Top.35 Top.36 Top.37} =
+Type@{Top.34} -> Type@{Top.37}
+     : Type@{max(Top.34+1, Top.37+1)}
+(* Top.34 Top.35 Top.36 Top.37 |= Top.34 < Top.35
+                                  Top.36 < Top.34
+                                  Top.37 < Top.36
+                                   *) *)
 Fail Check @qux@{Set Set}.
 Check @qux@{Type Type Type Type}.
 (* [qux] should only need two universes *)
diff --git a/test-suite/bugs/closed/5717.v b/test-suite/bugs/closed/5717.v
new file mode 100644
index 0000000000..1bfd917d25
--- /dev/null
+++ b/test-suite/bugs/closed/5717.v
@@ -0,0 +1,5 @@
+Definition foo@{i} (A : Type@{i}) (l : list A) :=
+  match l with
+  | nil => nil
+  | cons _ t => t
+  end.
-- 
cgit v1.2.3


From 280c922fc55b57c430cad721c83650a796a375fd Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Wed, 20 Sep 2017 19:45:43 +0200
Subject: Allow local universe renaming in Print.

---
 test-suite/output/UnivBinders.out | 31 +++++++++++++++++++++++++++++++
 test-suite/output/UnivBinders.v   | 19 +++++++++++++++++++
 2 files changed, 50 insertions(+)

(limited to 'test-suite')

diff --git a/test-suite/output/UnivBinders.out b/test-suite/output/UnivBinders.out
index 42fb52a3b3..6fb8cba187 100644
--- a/test-suite/output/UnivBinders.out
+++ b/test-suite/output/UnivBinders.out
@@ -53,3 +53,34 @@ Monomorphic mono = Type@{u}
 (* {u} |=  *)
 
 mono is not universe polymorphic
+foo@{E M N} = 
+Type@{M} -> Type@{N} -> Type@{E}
+     : Type@{max(E+1, M+1, N+1)}
+(* E M N |=  *)
+
+foo is universe polymorphic
+foo@{Top.16 Top.17 Top.18} = 
+Type@{Top.17} -> Type@{Top.18} -> Type@{Top.16}
+     : Type@{max(Top.16+1, Top.17+1, Top.18+1)}
+(* Top.16 Top.17 Top.18 |=  *)
+
+foo is universe polymorphic
+NonCumulative Inductive Empty@{E} : Type@{E} :=  
+NonCumulative Record PWrap (A : Type@{E}) : Type@{E} := pwrap { punwrap : A }
+
+PWrap has primitive projections with eta conversion.
+For PWrap: Argument scope is [type_scope]
+For pwrap: Argument scopes are [type_scope _]
+punwrap@{K} : forall A : Type@{K}, PWrap@{K} A -> A
+(* K |=  *)
+
+punwrap is universe polymorphic
+Argument scopes are [type_scope _]
+punwrap is transparent
+Expands to: Constant Top.punwrap
+The command has indeed failed with message:
+Universe instance should have length 3
+The command has indeed failed with message:
+Universe instance should have length 0
+The command has indeed failed with message:
+This object does not support universe names.
diff --git a/test-suite/output/UnivBinders.v b/test-suite/output/UnivBinders.v
index 2c378e795d..46904b3846 100644
--- a/test-suite/output/UnivBinders.v
+++ b/test-suite/output/UnivBinders.v
@@ -33,3 +33,22 @@ Print foo.
 (* Binders even work with monomorphic definitions! *)
 Monomorphic Definition mono@{u} := Type@{u}.
 Print mono.
+
+(* Using local binders for printing. *)
+Print foo@{E M N}.
+(* Underscores discard the name if there's one. *)
+Print foo@{_ _ _}.
+
+(* Also works for inductives and records. *)
+Print Empty@{E}.
+Print PWrap@{E}.
+
+(* Also works for About. *)
+About punwrap@{K}.
+
+(* Instance length check. *)
+Fail Print foo@{E}.
+Fail Print mono@{E}.
+
+(* Not everything can be printed with custom universe names. *)
+Fail Print Coq.Init.Logic@{E}.
-- 
cgit v1.2.3


From 765392492df2f5e065b2b5e706b6620846337cc0 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Thu, 21 Sep 2017 00:53:10 +0200
Subject: Universe binders survive sections, modules and compilation.

---
 test-suite/Makefile                  |  3 ++-
 test-suite/output/UnivBinders.out    | 41 ++++++++++++++++++++++++++++++++++++
 test-suite/output/UnivBinders.v      | 27 ++++++++++++++++++++++++
 test-suite/prerequisite/bind_univs.v |  5 +++++
 4 files changed, 75 insertions(+), 1 deletion(-)
 create mode 100644 test-suite/prerequisite/bind_univs.v

(limited to 'test-suite')

diff --git a/test-suite/Makefile b/test-suite/Makefile
index f169f86e88..6865dcc768 100644
--- a/test-suite/Makefile
+++ b/test-suite/Makefile
@@ -95,7 +95,8 @@ VSUBSYSTEMS := prerequisite success failure $(BUGS) output \
 SUBSYSTEMS := $(VSUBSYSTEMS) misc bugs ide vio coqchk coqwc coq-makefile
 
 PREREQUISITELOG = prerequisite/admit.v.log			\
-  prerequisite/make_local.v.log prerequisite/make_notation.v.log
+  prerequisite/make_local.v.log prerequisite/make_notation.v.log \
+  prerequisite/bind_univs.v.log
 
 #######################################################################
 # Phony targets
diff --git a/test-suite/output/UnivBinders.out b/test-suite/output/UnivBinders.out
index 6fb8cba187..04bd169bd3 100644
--- a/test-suite/output/UnivBinders.out
+++ b/test-suite/output/UnivBinders.out
@@ -84,3 +84,44 @@ The command has indeed failed with message:
 Universe instance should have length 0
 The command has indeed failed with message:
 This object does not support universe names.
+Monomorphic bind_univs.mono = Type@{u}
+     : Type@{u+1}
+(* {u} |=  *)
+
+bind_univs.mono is not universe polymorphic
+bind_univs.poly@{u} = Type@{u}
+     : Type@{u+1}
+(* u |=  *)
+
+bind_univs.poly is universe polymorphic
+insec@{v} = Type@{u} -> Type@{v}
+     : Type@{max(u+1, v+1)}
+(* v |=  *)
+
+insec is universe polymorphic
+insec@{u v} = Type@{u} -> Type@{v}
+     : Type@{max(u+1, v+1)}
+(* u v |=  *)
+
+insec is universe polymorphic
+inmod@{u} = Type@{u}
+     : Type@{u+1}
+(* u |=  *)
+
+inmod is universe polymorphic
+SomeMod.inmod@{u} = Type@{u}
+     : Type@{u+1}
+(* u |=  *)
+
+SomeMod.inmod is universe polymorphic
+inmod@{u} = Type@{u}
+     : Type@{u+1}
+(* u |=  *)
+
+inmod is universe polymorphic
+Applied.infunct@{u v} = 
+inmod@{u} -> Type@{v}
+     : Type@{max(u+1, v+1)}
+(* u v |=  *)
+
+Applied.infunct is universe polymorphic
diff --git a/test-suite/output/UnivBinders.v b/test-suite/output/UnivBinders.v
index 46904b3846..f0a9909868 100644
--- a/test-suite/output/UnivBinders.v
+++ b/test-suite/output/UnivBinders.v
@@ -52,3 +52,30 @@ Fail Print mono@{E}.
 
 (* Not everything can be printed with custom universe names. *)
 Fail Print Coq.Init.Logic@{E}.
+
+(* Universe binders survive through compilation, sections and modules. *)
+Require bind_univs.
+Print bind_univs.mono.
+Print bind_univs.poly.
+
+Section SomeSec.
+  Universe u.
+  Definition insec@{v} := Type@{u} -> Type@{v}.
+  Print insec.
+End SomeSec.
+Print insec.
+
+Module SomeMod.
+  Definition inmod@{u} := Type@{u}.
+  Print inmod.
+End SomeMod.
+Print SomeMod.inmod.
+Import SomeMod.
+Print inmod.
+
+Module Type SomeTyp. Definition inmod := Type. End SomeTyp.
+Module SomeFunct (In : SomeTyp).
+  Definition infunct@{u v} := In.inmod@{u} -> Type@{v}.
+End SomeFunct.
+Module Applied := SomeFunct(SomeMod).
+Print Applied.infunct.
diff --git a/test-suite/prerequisite/bind_univs.v b/test-suite/prerequisite/bind_univs.v
new file mode 100644
index 0000000000..f17c00e9d7
--- /dev/null
+++ b/test-suite/prerequisite/bind_univs.v
@@ -0,0 +1,5 @@
+(* Used in output/UnivBinders.v *)
+
+Monomorphic Definition mono@{u} := Type@{u}.
+
+Polymorphic Definition poly@{u} := Type@{u}.
-- 
cgit v1.2.3


From d071eac98b7812ac5c03004b438022900885d874 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Thu, 21 Sep 2017 11:14:11 +0200
Subject: Forbid repeated names in universe binders.

---
 test-suite/output/UnivBinders.out | 2 ++
 test-suite/output/UnivBinders.v   | 3 +++
 2 files changed, 5 insertions(+)

(limited to 'test-suite')

diff --git a/test-suite/output/UnivBinders.out b/test-suite/output/UnivBinders.out
index 04bd169bd3..a2857294b2 100644
--- a/test-suite/output/UnivBinders.out
+++ b/test-suite/output/UnivBinders.out
@@ -53,6 +53,8 @@ Monomorphic mono = Type@{u}
 (* {u} |=  *)
 
 mono is not universe polymorphic
+The command has indeed failed with message:
+Universe u already bound.
 foo@{E M N} = 
 Type@{M} -> Type@{N} -> Type@{E}
      : Type@{max(E+1, M+1, N+1)}
diff --git a/test-suite/output/UnivBinders.v b/test-suite/output/UnivBinders.v
index f0a9909868..013f215b51 100644
--- a/test-suite/output/UnivBinders.v
+++ b/test-suite/output/UnivBinders.v
@@ -34,6 +34,9 @@ Print foo.
 Monomorphic Definition mono@{u} := Type@{u}.
 Print mono.
 
+(* fun x x => foo is nonsense with local binders *)
+Fail Definition fo@{u u} := Type@{u}.
+
 (* Using local binders for printing. *)
 Print foo@{E M N}.
 (* Underscores discard the name if there's one. *)
-- 
cgit v1.2.3


From f8e639f3b81ae142f5b529be1ad90210fc259375 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Thu, 28 Sep 2017 22:28:21 +0200
Subject: Fix interpretation of global universes in univdecl constraints.

Also nicer error when the constraints are impossible.
---
 test-suite/output/UnivBinders.out | 2 ++
 test-suite/output/UnivBinders.v   | 4 ++++
 test-suite/success/polymorphism.v | 4 ++++
 3 files changed, 10 insertions(+)

(limited to 'test-suite')

diff --git a/test-suite/output/UnivBinders.out b/test-suite/output/UnivBinders.out
index a2857294b2..9eb162fc0f 100644
--- a/test-suite/output/UnivBinders.out
+++ b/test-suite/output/UnivBinders.out
@@ -86,6 +86,8 @@ The command has indeed failed with message:
 Universe instance should have length 0
 The command has indeed failed with message:
 This object does not support universe names.
+The command has indeed failed with message:
+Cannot enforce v < u because u < gU < gV < v
 Monomorphic bind_univs.mono = Type@{u}
      : Type@{u+1}
 (* {u} |=  *)
diff --git a/test-suite/output/UnivBinders.v b/test-suite/output/UnivBinders.v
index 013f215b51..a65a1fdf36 100644
--- a/test-suite/output/UnivBinders.v
+++ b/test-suite/output/UnivBinders.v
@@ -56,6 +56,10 @@ Fail Print mono@{E}.
 (* Not everything can be printed with custom universe names. *)
 Fail Print Coq.Init.Logic@{E}.
 
+(* Nice error when constraints are impossible. *)
+Monomorphic Universes gU gV. Monomorphic Constraint gU < gV.
+Fail Lemma foo@{u v|u < gU, gV < v, v < u} : nat.
+
 (* Universe binders survive through compilation, sections and modules. *)
 Require bind_univs.
 Print bind_univs.mono.
diff --git a/test-suite/success/polymorphism.v b/test-suite/success/polymorphism.v
index c09a60a4d7..b3f9a4994c 100644
--- a/test-suite/success/polymorphism.v
+++ b/test-suite/success/polymorphism.v
@@ -202,6 +202,10 @@ Module binders.
     exact Type@{i}.
   Qed.
 
+  Monomorphic Universe M.
+  Fail Definition with_mono@{u|} : Type@{M} := Type@{u}.
+  Definition with_mono@{u|u < M} : Type@{M} := Type@{u}.
+
 End binders.
     
 Section cats.
-- 
cgit v1.2.3


From 4940f99922b0784d726b7c50abe63395713f012f Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Fri, 17 Nov 2017 23:48:21 +0100
Subject: Fix #5347: unify declaration of axioms with and without bound univs.

Note that this makes the following syntax valid:

     Axiom foo@{i} bar : Type@{i}.

(ie putting a universe declaration on the first axiom in the list, the
declaration then holds for the whole list).
---
 test-suite/bugs/closed/5347.v     | 10 ++++++++++
 test-suite/output/UnivBinders.out | 24 ++++++++++++++++++++++++
 test-suite/output/UnivBinders.v   | 13 +++++++++++++
 3 files changed, 47 insertions(+)
 create mode 100644 test-suite/bugs/closed/5347.v

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/5347.v b/test-suite/bugs/closed/5347.v
new file mode 100644
index 0000000000..9267b3eb69
--- /dev/null
+++ b/test-suite/bugs/closed/5347.v
@@ -0,0 +1,10 @@
+Set Universe Polymorphism.
+
+Axiom X : Type.
+(* Used to declare [x0@{u1 u2} : X@{u1}] and [x1@{} : X@{u2}] leaving
+   the type of x1 with undeclared universes. After PR #891 this should
+   error at declaration time. *)
+Axiom x₀ x₁ : X.
+Axiom Xᵢ : X -> Type.
+
+Check Xᵢ x₁. (* conversion test raised anomaly universe undefined *)
diff --git a/test-suite/output/UnivBinders.out b/test-suite/output/UnivBinders.out
index 9eb162fc0f..f69379a571 100644
--- a/test-suite/output/UnivBinders.out
+++ b/test-suite/output/UnivBinders.out
@@ -129,3 +129,27 @@ inmod@{u} -> Type@{v}
 (* u v |=  *)
 
 Applied.infunct is universe polymorphic
+axfoo@{i Top.33 Top.34} : Type@{Top.33} -> Type@{i}
+(* i Top.33 Top.34 |=  *)
+
+axfoo is universe polymorphic
+Argument scope is [type_scope]
+Expands to: Constant Top.axfoo
+axbar@{i Top.33 Top.34} : Type@{Top.34} -> Type@{i}
+(* i Top.33 Top.34 |=  *)
+
+axbar is universe polymorphic
+Argument scope is [type_scope]
+Expands to: Constant Top.axbar
+axfoo' : Type@{Top.36} -> Type@{i}
+
+axfoo' is not universe polymorphic
+Argument scope is [type_scope]
+Expands to: Constant Top.axfoo'
+axbar' : Type@{Top.36} -> Type@{i}
+
+axbar' is not universe polymorphic
+Argument scope is [type_scope]
+Expands to: Constant Top.axbar'
+The command has indeed failed with message:
+When declaring multiple axioms in one command, only the first is allowed a universe binder (which will be shared by the whole block).
diff --git a/test-suite/output/UnivBinders.v b/test-suite/output/UnivBinders.v
index a65a1fdf36..116d5e5e94 100644
--- a/test-suite/output/UnivBinders.v
+++ b/test-suite/output/UnivBinders.v
@@ -86,3 +86,16 @@ Module SomeFunct (In : SomeTyp).
 End SomeFunct.
 Module Applied := SomeFunct(SomeMod).
 Print Applied.infunct.
+
+(* Multi-axiom declaration
+
+   In polymorphic mode the domain Type gets separate universes for the
+   different axioms, but all axioms have to declare all universes. In
+   polymorphic mode they get the same universes, ie the type is only
+   interpd once. *)
+Axiom axfoo@{i+} axbar : Type -> Type@{i}.
+Monomorphic Axiom axfoo'@{i+} axbar' : Type -> Type@{i}.
+
+About axfoo. About axbar. About axfoo'. About axbar'.
+
+Fail Axiom failfoo failbar@{i} : Type.
-- 
cgit v1.2.3


From edb2b2535d62b37c324c98b28802c1b1699d4014 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Sat, 25 Nov 2017 22:08:01 +0100
Subject: Restrict universe context when declaring constants in obligations.

---
 test-suite/success/polymorphism.v | 7 +++++++
 1 file changed, 7 insertions(+)

(limited to 'test-suite')

diff --git a/test-suite/success/polymorphism.v b/test-suite/success/polymorphism.v
index b3f9a4994c..d76b307914 100644
--- a/test-suite/success/polymorphism.v
+++ b/test-suite/success/polymorphism.v
@@ -461,3 +461,10 @@ Section test_letin_subtyping.
   Qed.
 
 End test_letin_subtyping.
+
+Module ObligationRegression.
+  (** Test for a regression encountered when fixing obligations for
+      stronger restriction of universe context. *)
+  Require Import CMorphisms.
+  Check trans_co_eq_inv_arrow_morphism@{_ _ _ _ _  _ _ _}.
+End ObligationRegression.
-- 
cgit v1.2.3