From 280c922fc55b57c430cad721c83650a796a375fd Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
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 42fb52a3b..6fb8cba18 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 2c378e795..46904b384 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