Clean UnivBinders test

- rename @{u} to @{uu} (u is the default name so using @{u} doesn't
  test as much as it should)

- move part of the test using Require to end of the file (when quickly
  testing changes this allows to run most of the test without compiling
  the Require'd file)

test-suite/output/UnivBinders.out

@@ -1,85 +1,85 @@
-Inductive Empty@{u} : Type@{u} :=  
-(* u |=  *)
-Record PWrap (A : Type@{u}) : Type@{u} := pwrap { punwrap : A }
-(* u |=  *)
+Inductive Empty@{uu} : Type@{uu} :=  
+(* uu |=  *)
+Record PWrap (A : Type@{uu}) : Type@{uu} := pwrap { punwrap : A }
+(* uu |=  *)
 
 PWrap has primitive projections with eta conversion.
 Arguments PWrap _%type_scope
 Arguments pwrap _%type_scope _
-punwrap@{u} = 
-fun (A : Type@{u}) (p : PWrap@{u} A) => punwrap _ p
-     : forall A : Type@{u}, PWrap@{u} A -> A
-(* u |=  *)
+punwrap@{uu} = 
+fun (A : Type@{uu}) (p : PWrap@{uu} A) => punwrap _ p
+     : forall A : Type@{uu}, PWrap@{uu} A -> A
+(* uu |=  *)
 
 Arguments punwrap _%type_scope _
-Record RWrap (A : Type@{u}) : Type@{u} := rwrap { runwrap : A }
-(* u |=  *)
+Record RWrap (A : Type@{uu}) : Type@{uu} := rwrap { runwrap : A }
+(* uu |=  *)
 
 Arguments RWrap _%type_scope
 Arguments rwrap _%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@{uu} = 
+fun (A : Type@{uu}) (r : RWrap@{uu} A) => let (runwrap) := r in runwrap
+     : forall A : Type@{uu}, RWrap@{uu} A -> A
+(* uu |=  *)
 
 Arguments runwrap _%type_scope _
-Wrap@{u} = fun A : Type@{u} => A
-     : Type@{u} -> Type@{u}
-(* u |=  *)
+Wrap@{uu} = fun A : Type@{uu} => A
+     : Type@{uu} -> Type@{uu}
+(* uu |=  *)
 
 Arguments Wrap _%type_scope
-wrap@{u} = 
-fun (A : Type@{u}) (Wrap : Wrap@{u} A) => Wrap
-     : forall A : Type@{u}, Wrap@{u} A -> A
-(* u |=  *)
+wrap@{uu} = 
+fun (A : Type@{uu}) (Wrap : Wrap@{uu} A) => Wrap
+     : forall A : Type@{uu}, Wrap@{uu} A -> A
+(* uu |=  *)
 
 Arguments wrap {A}%type_scope {Wrap}
-bar@{u} = nat
-     : Wrap@{u} Set
-(* u |= Set < u *)
-foo@{u u0 v} = 
-Type@{u0} -> Type@{v} -> Type@{u}
-     : Type@{max(u+1,u0+1,v+1)}
-(* u u0 v |=  *)
+bar@{uu} = nat
+     : Wrap@{uu} Set
+(* uu |= Set < uu *)
+foo@{uu u v} = 
+Type@{u} -> Type@{v} -> Type@{uu}
+     : Type@{max(uu+1,u+1,v+1)}
+(* uu u v |=  *)
 Type@{i} -> Type@{j}
      : Type@{max(i+1,j+1)}
 (* {j i} |=  *)
      = Type@{i} -> Type@{j}
      : Type@{max(i+1,j+1)}
 (* {j i} |=  *)
-mono = Type@{mono.u}
-     : Type@{mono.u+1}
-(* {mono.u} |=  *)
+mono = Type@{mono.uu}
+     : Type@{mono.uu+1}
+(* {mono.uu} |=  *)
 mono
-     : Type@{mono.u+1}
-Type@{mono.u}
-     : Type@{mono.u+1}
+     : Type@{mono.uu+1}
+Type@{mono.uu}
+     : Type@{mono.uu+1}
 The command has indeed failed with message:
-Universe u already exists.
+Universe uu already exists.
 monomono
      : Type@{MONOU+1}
 mono.monomono
      : Type@{mono.MONOU+1}
 monomono
      : Type@{MONOU+1}
 mono
-     : Type@{mono.u+1}
+     : Type@{mono.uu+1}
 The command has indeed failed with message:
-Universe u already exists.
+Universe uu already exists.
 bobmorane = 
 let tt := Type@{UnivBinders.32} in
 let ff := Type@{UnivBinders.34} in tt -> ff
      : Type@{max(UnivBinders.31,UnivBinders.33)}
 The command has indeed failed with message:
-Universe u already bound.
+Universe uu already bound.
 foo@{E M N} = 
 Type@{M} -> Type@{N} -> Type@{E}
      : Type@{max(E+1,M+1,N+1)}
 (* E M N |=  *)
-foo@{u u0 v} = 
-Type@{u0} -> Type@{v} -> Type@{u}
-     : Type@{max(u+1,u0+1,v+1)}
-(* u u0 v |=  *)
+foo@{uu u v} = 
+Type@{u} -> Type@{v} -> Type@{uu}
+     : Type@{max(uu+1,u+1,v+1)}
+(* uu u v |=  *)
 Inductive Empty@{E} : Type@{E} :=  
 (* E |=  *)
 Record PWrap (A : Type@{E}) : Type@{E} := pwrap { punwrap : A }
@@ -103,45 +103,38 @@ 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
-bind_univs.mono = 
-Type@{bind_univs.mono.u}
-     : Type@{bind_univs.mono.u+1}
-(* {bind_univs.mono.u} |=  *)
-bind_univs.poly@{u} = Type@{u}
-     : Type@{u+1}
-(* u |=  *)
-insec@{v} = Type@{u} -> Type@{v}
-     : Type@{max(u+1,v+1)}
+insec@{v} = Type@{uu} -> Type@{v}
+     : Type@{max(uu+1,v+1)}
 (* v |=  *)
 Inductive insecind@{k} : Type@{k+1} :=
     inseccstr : Type@{k} -> insecind@{k}
 (* k |=  *)
 
 Arguments inseccstr _%type_scope
-insec@{u v} = Type@{u} -> Type@{v}
-     : Type@{max(u+1,v+1)}
-(* u v |=  *)
-Inductive insecind@{u k} : Type@{k+1} :=
-    inseccstr : Type@{k} -> insecind@{u k}
-(* u k |=  *)
+insec@{uu v} = Type@{uu} -> Type@{v}
+     : Type@{max(uu+1,v+1)}
+(* uu v |=  *)
+Inductive insecind@{uu k} : Type@{k+1} :=
+    inseccstr : Type@{k} -> insecind@{uu k}
+(* uu k |=  *)
 
 Arguments inseccstr _%type_scope
 insec2@{u} = Prop
      : Type@{Set+1}
 (* u |=  *)
-inmod@{u} = Type@{u}
-     : Type@{u+1}
-(* u |=  *)
-SomeMod.inmod@{u} = Type@{u}
-     : Type@{u+1}
-(* u |=  *)
-inmod@{u} = Type@{u}
-     : Type@{u+1}
-(* u |=  *)
-Applied.infunct@{u v} = 
-inmod@{u} -> Type@{v}
-     : Type@{max(u+1,v+1)}
-(* u v |=  *)
+inmod@{uu} = Type@{uu}
+     : Type@{uu+1}
+(* uu |=  *)
+SomeMod.inmod@{uu} = Type@{uu}
+     : Type@{uu+1}
+(* uu |=  *)
+inmod@{uu} = Type@{uu}
+     : Type@{uu+1}
+(* uu |=  *)
+Applied.infunct@{uu v} = 
+inmod@{uu} -> Type@{v}
+     : Type@{max(uu+1,v+1)}
+(* uu v |=  *)
 axfoo@{i u u0} : Type@{u} -> Type@{i}
 (* i u u0 |=  *)
 
@@ -166,3 +159,10 @@ Arguments axbar' _%type_scope
 Expands to: Constant UnivBinders.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).
+bind_univs.mono = 
+Type@{bind_univs.mono.u}
+     : Type@{bind_univs.mono.u+1}
+(* {bind_univs.mono.u} |=  *)
+bind_univs.poly@{u} = Type@{u}
+     : Type@{u+1}
+(* u |=  *)

test-suite/output/UnivBinders.v

@@ -5,32 +5,32 @@ Set Printing Universes.
 (* Unset Strict Universe Declaration. *)
 
 (* universe binders on inductive types and record projections *)
-Inductive Empty@{u} : Type@{u} := .
+Inductive Empty@{uu} : Type@{uu} := .
 Print Empty.
 
 Set Primitive Projections.
-Record PWrap@{u} (A:Type@{u}) := pwrap { punwrap : A }.
+Record PWrap@{uu} (A:Type@{uu}) := pwrap { punwrap : A }.
 Print PWrap.
 Print punwrap.
 
 Unset Primitive Projections.
-Record RWrap@{u} (A:Type@{u}) := rwrap { runwrap : A }.
+Record RWrap@{uu} (A:Type@{uu}) := 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.
+Class Wrap@{uu} (A:Type@{uu}) := 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.
+Instance bar@{uu} : Wrap@{uu} Set. Proof. exact nat. Qed.
 Print bar.
 
 Unset Strict Universe Declaration.
 (* The universes in the binder come first, then the extra universes in
    order of appearance. *)
-Definition foo@{u +} := Type -> Type@{v} -> Type@{u}.
+Definition foo@{uu +} := Type -> Type@{v} -> Type@{uu}.
 Print foo.
 
 Check Type@{i} -> Type@{j}.
@@ -40,13 +40,13 @@ Eval cbv in Type@{i} -> Type@{j}.
 Set Strict Universe Declaration.
 
 (* Binders even work with monomorphic definitions! *)
-Monomorphic Definition mono@{u} := Type@{u}.
+Monomorphic Definition mono@{uu} := Type@{uu}.
 Print mono.
 Check mono.
-Check Type@{mono.u}.
+Check Type@{mono.uu}.
 
 Module mono.
-  Fail Monomorphic Universe u.
+  Fail Monomorphic Universe uu.
   Monomorphic Universe MONOU.
 
   Monomorphic Definition monomono := Type@{MONOU}.
@@ -60,28 +60,28 @@ Import mono.
 Check monomono. (* unqualified MONOU *)
 Check mono. (* still qualified mono.u *)
 
-Monomorphic Constraint Set < UnivBinders.mono.u.
+Monomorphic Constraint Set < UnivBinders.mono.uu.
 
 Module mono2.
-  Monomorphic Universe u.
+  Monomorphic Universe uu.
 End mono2.
 
-Fail Monomorphic Definition mono2@{u} := Type@{u}.
+Fail Monomorphic Definition mono2@{uu} := Type@{uu}.
 
 Module SecLet.
   Unset Universe Polymorphism.
   Section foo.
-    (* Fail Let foo@{} := Type@{u}. (* doesn't parse: Let foo@{...} doesn't exist *) *)
+    (* Fail Let foo@{} := Type@{uu}. (* doesn't parse: Let foo@{...} doesn't exist *) *)
     Unset Strict Universe Declaration.
-    Let tt : Type@{u} := Type@{v}. (* names disappear in the ether *)
-    Let ff : Type@{u}. Proof. exact Type@{v}. Qed. (* names disappear into space *)
+    Let tt : Type@{uu} := Type@{v}. (* names disappear in the ether *)
+    Let ff : Type@{uu}. Proof. exact Type@{v}. Qed. (* names disappear into space *)
     Definition bobmorane := tt -> ff.
   End foo.
   Print bobmorane.
 End SecLet.
 
 (* fun x x => foo is nonsense with local binders *)
-Fail Definition fo@{u u} := Type@{u}.
+Fail Definition fo@{uu uu} := Type@{uu}.
 
 (* Using local binders for printing. *)
 Print foo@{E M N}.
@@ -106,14 +106,9 @@ Fail Print Coq.Init.Logic@{E}.
 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 TestSuite.bind_univs.
-Print bind_univs.mono.
-Print bind_univs.poly.
-
 Section SomeSec.
-  Universe u.
-  Definition insec@{v} := Type@{u} -> Type@{v}.
+  Universe uu.
+  Definition insec@{v} := Type@{uu} -> Type@{v}.
   Print insec.
 
   Inductive insecind@{k} := inseccstr : Type@{k} -> insecind.
@@ -129,7 +124,7 @@ End SomeSec2.
 Print insec2.
 
 Module SomeMod.
-  Definition inmod@{u} := Type@{u}.
+  Definition inmod@{uu} := Type@{uu}.
   Print inmod.
 End SomeMod.
 Print SomeMod.inmod.
@@ -138,7 +133,7 @@ Print inmod.
 
 Module Type SomeTyp. Definition inmod := Type. End SomeTyp.
 Module SomeFunct (In : SomeTyp).
-  Definition infunct@{u v} := In.inmod@{u} -> Type@{v}.
+  Definition infunct@{uu v} := In.inmod@{uu} -> Type@{v}.
 End SomeFunct.
 Module Applied := SomeFunct(SomeMod).
 Print Applied.infunct.
@@ -147,11 +142,16 @@ Print Applied.infunct.
 
    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
+   monomorphic 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.
+
+(* Universe binders survive through compilation, sections and modules. *)
+Require TestSuite.bind_univs.
+Print bind_univs.mono.
+Print bind_univs.poly.