aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--printing/prettyp.ml12
-rw-r--r--test-suite/output/Arguments.out13
-rw-r--r--test-suite/output/ArgumentsScope.out14
-rw-r--r--test-suite/output/Arguments_renaming.out7
-rw-r--r--test-suite/output/Cases.out9
-rw-r--r--test-suite/output/Implicit.out1
-rw-r--r--test-suite/output/PrintInfos.out9
-rw-r--r--test-suite/output/TranspModtype.out8
-rw-r--r--test-suite/output/inference.out2
9 files changed, 7 insertions, 68 deletions
diff --git a/printing/prettyp.ml b/printing/prettyp.ml
index 0e6c595e1..4a66c33df 100644
--- a/printing/prettyp.ml
+++ b/printing/prettyp.ml
@@ -197,11 +197,13 @@ let print_opacity ref =
let print_polymorphism ref =
let poly = Global.is_polymorphic ref in
let template_poly = Global.is_template_polymorphic ref in
- pr_global ref ++ str " is " ++ str
+ if Flags.is_universe_polymorphism () || poly || template_poly then
+ [ pr_global ref ++ str " is " ++ str
(if poly then "universe polymorphic"
else if template_poly then
"template universe polymorphic"
- else "not universe polymorphic")
+ else "not universe polymorphic") ]
+ else []
let print_primitive_record mipv = function
| Some (Some (_, ps,_)) ->
@@ -214,9 +216,8 @@ let print_primitive ref =
let mib,_ = Global.lookup_inductive ind in
print_primitive_record mib.mind_packets mib.mind_record
| _ -> []
-
+
let print_name_infos ref =
- let poly = print_polymorphism ref in
let impls = implicits_of_global ref in
let scopes = Notation.find_arguments_scope ref in
let renames =
@@ -228,7 +229,8 @@ let print_name_infos ref =
print_ref true ref; blankline]
else
[] in
- poly :: print_primitive ref @
+ print_polymorphism ref @
+ print_primitive ref @
type_info_for_implicit @
print_renames_list (mt()) renames @
print_impargs_list (mt()) impls @
diff --git a/test-suite/output/Arguments.out b/test-suite/output/Arguments.out
index 9c488ce5a..2c7b04c62 100644
--- a/test-suite/output/Arguments.out
+++ b/test-suite/output/Arguments.out
@@ -1,13 +1,11 @@
Nat.sub : nat -> nat -> nat
-Nat.sub is not universe polymorphic
Argument scopes are [nat_scope nat_scope]
The reduction tactics unfold Nat.sub but avoid exposing match constructs
Nat.sub is transparent
Expands to: Constant Coq.Init.Nat.sub
Nat.sub : nat -> nat -> nat
-Nat.sub is not universe polymorphic
Argument scopes are [nat_scope nat_scope]
The reduction tactics unfold Nat.sub when applied to 1 argument
but avoid exposing match constructs
@@ -15,7 +13,6 @@ Nat.sub is transparent
Expands to: Constant Coq.Init.Nat.sub
Nat.sub : nat -> nat -> nat
-Nat.sub is not universe polymorphic
Argument scopes are [nat_scope nat_scope]
The reduction tactics unfold Nat.sub
when the 1st argument evaluates to a constructor and
@@ -24,7 +21,6 @@ Nat.sub is transparent
Expands to: Constant Coq.Init.Nat.sub
Nat.sub : nat -> nat -> nat
-Nat.sub is not universe polymorphic
Argument scopes are [nat_scope nat_scope]
The reduction tactics unfold Nat.sub when the 1st and
2nd arguments evaluate to a constructor and when applied to 2 arguments
@@ -32,7 +28,6 @@ Nat.sub is transparent
Expands to: Constant Coq.Init.Nat.sub
Nat.sub : nat -> nat -> nat
-Nat.sub is not universe polymorphic
Argument scopes are [nat_scope nat_scope]
The reduction tactics unfold Nat.sub when the 1st and
2nd arguments evaluate to a constructor
@@ -42,7 +37,6 @@ pf :
forall D1 C1 : Type,
(D1 -> C1) -> forall D2 C2 : Type, (D2 -> C2) -> D1 * D2 -> C1 * C2
-pf is not universe polymorphic
Arguments D2, C2 are implicit
Arguments D1, C1 are implicit and maximally inserted
Argument scopes are [foo_scope type_scope _ _ _ _ _]
@@ -51,7 +45,6 @@ pf is transparent
Expands to: Constant Top.pf
fcomp : forall A B C : Type, (B -> C) -> (A -> B) -> A -> C
-fcomp is not universe polymorphic
Arguments A, B, C are implicit and maximally inserted
Argument scopes are [type_scope type_scope type_scope _ _ _]
The reduction tactics unfold fcomp when applied to 6 arguments
@@ -59,20 +52,17 @@ fcomp is transparent
Expands to: Constant Top.fcomp
volatile : nat -> nat
-volatile is not universe polymorphic
Argument scope is [nat_scope]
The reduction tactics always unfold volatile
volatile is transparent
Expands to: Constant Top.volatile
f : T1 -> T2 -> nat -> unit -> nat -> nat
-f is not universe polymorphic
Argument scopes are [_ _ nat_scope _ nat_scope]
f is transparent
Expands to: Constant Top.S1.S2.f
f : T1 -> T2 -> nat -> unit -> nat -> nat
-f is not universe polymorphic
Argument scopes are [_ _ nat_scope _ nat_scope]
The reduction tactics unfold f when the 3rd, 4th and
5th arguments evaluate to a constructor
@@ -80,7 +70,6 @@ f is transparent
Expands to: Constant Top.S1.S2.f
f : forall T2 : Type, T1 -> T2 -> nat -> unit -> nat -> nat
-f is not universe polymorphic
Argument T2 is implicit
Argument scopes are [type_scope _ _ nat_scope _ nat_scope]
The reduction tactics unfold f when the 4th, 5th and
@@ -89,7 +78,6 @@ f is transparent
Expands to: Constant Top.S1.f
f : forall T1 T2 : Type, T1 -> T2 -> nat -> unit -> nat -> nat
-f is not universe polymorphic
Arguments T1, T2 are implicit
Argument scopes are [type_scope type_scope _ _ nat_scope _ nat_scope]
The reduction tactics unfold f when the 5th, 6th and
@@ -102,7 +90,6 @@ Expands to: Constant Top.f
: Prop
f : forall T1 T2 : Type, T1 -> T2 -> nat -> unit -> nat -> nat
-f is not universe polymorphic
The reduction tactics unfold f when the 5th, 6th and
7th arguments evaluate to a constructor
f is transparent
diff --git a/test-suite/output/ArgumentsScope.out b/test-suite/output/ArgumentsScope.out
index 71d5fc78b..6643c1429 100644
--- a/test-suite/output/ArgumentsScope.out
+++ b/test-suite/output/ArgumentsScope.out
@@ -1,70 +1,56 @@
a : bool -> bool
-a is not universe polymorphic
Argument scope is [bool_scope]
Expands to: Variable a
b : bool -> bool
-b is not universe polymorphic
Argument scope is [bool_scope]
Expands to: Variable b
negb'' : bool -> bool
-negb'' is not universe polymorphic
Argument scope is [bool_scope]
negb'' is transparent
Expands to: Constant Top.A.B.negb''
negb' : bool -> bool
-negb' is not universe polymorphic
Argument scope is [bool_scope]
negb' is transparent
Expands to: Constant Top.A.negb'
negb : bool -> bool
-negb is not universe polymorphic
Argument scope is [bool_scope]
negb is transparent
Expands to: Constant Coq.Init.Datatypes.negb
a : bool -> bool
-a is not universe polymorphic
Expands to: Variable a
b : bool -> bool
-b is not universe polymorphic
Expands to: Variable b
negb : bool -> bool
-negb is not universe polymorphic
negb is transparent
Expands to: Constant Coq.Init.Datatypes.negb
negb' : bool -> bool
-negb' is not universe polymorphic
negb' is transparent
Expands to: Constant Top.A.negb'
negb'' : bool -> bool
-negb'' is not universe polymorphic
negb'' is transparent
Expands to: Constant Top.A.B.negb''
a : bool -> bool
-a is not universe polymorphic
Expands to: Variable a
negb : bool -> bool
-negb is not universe polymorphic
negb is transparent
Expands to: Constant Coq.Init.Datatypes.negb
negb' : bool -> bool
-negb' is not universe polymorphic
negb' is transparent
Expands to: Constant Top.negb'
negb'' : bool -> bool
-negb'' is not universe polymorphic
negb'' is transparent
Expands to: Constant Top.negb''
diff --git a/test-suite/output/Arguments_renaming.out b/test-suite/output/Arguments_renaming.out
index 9331f29fb..1e3cc37df 100644
--- a/test-suite/output/Arguments_renaming.out
+++ b/test-suite/output/Arguments_renaming.out
@@ -20,7 +20,6 @@ For eq: Argument scopes are [type_scope _ _]
For eq_refl: Argument scopes are [type_scope _]
eq_refl : forall (A : Type) (x : A), x = x
-eq_refl is not universe polymorphic
Arguments are renamed to B, y
When applied to no arguments:
Arguments B, y are implicit and maximally inserted
@@ -36,7 +35,6 @@ For myEq: Argument scopes are [type_scope _ _]
For myrefl: Argument scopes are [type_scope _ _]
myrefl : forall (B : Type) (x : A), B -> myEq B x x
-myrefl is not universe polymorphic
Arguments are renamed to C, x, _
Argument C is implicit and maximally inserted
Argument scopes are [type_scope _ _]
@@ -49,13 +47,11 @@ fix myplus (T : Type) (t : T) (n m : nat) {struct n} : nat :=
end
: forall T : Type, T -> nat -> nat -> nat
-myplus is not universe polymorphic
Arguments are renamed to Z, t, n, m
Argument Z is implicit and maximally inserted
Argument scopes are [type_scope _ nat_scope nat_scope]
myplus : forall T : Type, T -> nat -> nat -> nat
-myplus is not universe polymorphic
Arguments are renamed to Z, t, n, m
Argument Z is implicit and maximally inserted
Argument scopes are [type_scope _ nat_scope nat_scope]
@@ -74,7 +70,6 @@ For myEq: Argument scopes are [type_scope type_scope _ _]
For myrefl: Argument scopes are [type_scope type_scope _ _]
myrefl : forall (A B : Type) (x : A), B -> myEq A B x x
-myrefl is not universe polymorphic
Arguments are renamed to A, C, x, _
Argument C is implicit and maximally inserted
Argument scopes are [type_scope type_scope _ _]
@@ -89,13 +84,11 @@ fix myplus (T : Type) (t : T) (n m : nat) {struct n} : nat :=
end
: forall T : Type, T -> nat -> nat -> nat
-myplus is not universe polymorphic
Arguments are renamed to Z, t, n, m
Argument Z is implicit and maximally inserted
Argument scopes are [type_scope _ nat_scope nat_scope]
myplus : forall T : Type, T -> nat -> nat -> nat
-myplus is not universe polymorphic
Arguments are renamed to Z, t, n, m
Argument Z is implicit and maximally inserted
Argument scopes are [type_scope _ nat_scope nat_scope]
diff --git a/test-suite/output/Cases.out b/test-suite/output/Cases.out
index d59034836..09f032d47 100644
--- a/test-suite/output/Cases.out
+++ b/test-suite/output/Cases.out
@@ -6,8 +6,6 @@ fix F (t : t) : P t :=
end
: forall P : t -> Type,
(let x := t in forall x0 : x, P x0 -> P (k x0)) -> forall t : t, P t
-
-t_rect is not universe polymorphic
= fun d : TT => match d with
| @CTT _ _ b => b
end
@@ -26,7 +24,6 @@ match Nat.eq_dec x y with
end
: forall (x y : nat) (P : nat -> Type), P x -> P y -> P y
-proj is not universe polymorphic
Argument scopes are [nat_scope nat_scope _ _ _]
foo =
fix foo (A : Type) (l : list A) {struct l} : option A :=
@@ -37,7 +34,6 @@ fix foo (A : Type) (l : list A) {struct l} : option A :=
end
: forall A : Type, list A -> option A
-foo is not universe polymorphic
Argument scopes are [type_scope list_scope]
uncast =
fun (A : Type) (x : I A) => match x with
@@ -45,12 +41,9 @@ fun (A : Type) (x : I A) => match x with
end
: forall A : Type, I A -> A
-uncast is not universe polymorphic
Argument scopes are [type_scope _]
foo' = if A 0 then true else false
: bool
-
-foo' is not universe polymorphic
f =
fun H : B =>
match H with
@@ -61,5 +54,3 @@ match H with
else fun _ : P false => Logic.I) x
end
: B -> True
-
-f is not universe polymorphic
diff --git a/test-suite/output/Implicit.out b/test-suite/output/Implicit.out
index 0b0f501f9..3b65003c2 100644
--- a/test-suite/output/Implicit.out
+++ b/test-suite/output/Implicit.out
@@ -5,7 +5,6 @@ ex_intro (P:=fun _ : nat => True) (x:=0) I
d2 = fun x : nat => d1 (y:=x)
: forall x x0 : nat, x0 = x -> x0 = x
-d2 is not universe polymorphic
Arguments x, x0 are implicit
Argument scopes are [nat_scope nat_scope _]
map id (1 :: nil)
diff --git a/test-suite/output/PrintInfos.out b/test-suite/output/PrintInfos.out
index 0457c860d..ba076f050 100644
--- a/test-suite/output/PrintInfos.out
+++ b/test-suite/output/PrintInfos.out
@@ -25,7 +25,6 @@ For eq: Argument scopes are [type_scope _ _]
For eq_refl: Argument scopes are [type_scope _]
eq_refl : forall (A : Type) (x : A), x = x
-eq_refl is not universe polymorphic
When applied to no arguments:
Arguments A, x are implicit and maximally inserted
When applied to 1 argument:
@@ -46,11 +45,9 @@ fix add (n m : nat) {struct n} : nat :=
end
: nat -> nat -> nat
-Nat.add is not universe polymorphic
Argument scopes are [nat_scope nat_scope]
Nat.add : nat -> nat -> nat
-Nat.add is not universe polymorphic
Argument scopes are [nat_scope nat_scope]
Nat.add is transparent
Expands to: Constant Coq.Init.Nat.add
@@ -58,7 +55,6 @@ Nat.add : nat -> nat -> nat
plus_n_O : forall n : nat, n = n + 0
-plus_n_O is not universe polymorphic
Argument scope is [nat_scope]
plus_n_O is opaque
Expands to: Constant Coq.Init.Peano.plus_n_O
@@ -80,13 +76,11 @@ For le_n: Argument scope is [nat_scope]
For le_S: Argument scopes are [nat_scope nat_scope _]
comparison : Set
-comparison is not universe polymorphic
Expands to: Inductive Coq.Init.Datatypes.comparison
Inductive comparison : Set :=
Eq : comparison | Lt : comparison | Gt : comparison
bar : foo
-bar is not universe polymorphic
Expanded type for implicit arguments
bar : forall x : nat, x = 0
@@ -94,14 +88,12 @@ Argument x is implicit and maximally inserted
Expands to: Constant Top.bar
*** [ bar : foo ]
-bar is not universe polymorphic
Expanded type for implicit arguments
bar : forall x : nat, x = 0
Argument x is implicit and maximally inserted
bar : foo
-bar is not universe polymorphic
Expanded type for implicit arguments
bar : forall x : nat, x = 0
@@ -109,7 +101,6 @@ Argument x is implicit and maximally inserted
Expands to: Constant Top.bar
*** [ bar : foo ]
-bar is not universe polymorphic
Expanded type for implicit arguments
bar : forall x : nat, x = 0
diff --git a/test-suite/output/TranspModtype.out b/test-suite/output/TranspModtype.out
index 67b65d4b8..f94ed6423 100644
--- a/test-suite/output/TranspModtype.out
+++ b/test-suite/output/TranspModtype.out
@@ -1,15 +1,7 @@
TrM.A = M.A
: Set
-
-TrM.A is not universe polymorphic
OpM.A = M.A
: Set
-
-OpM.A is not universe polymorphic
TrM.B = M.B
: Set
-
-TrM.B is not universe polymorphic
*** [ OpM.B : Set ]
-
-OpM.B is not universe polymorphic
diff --git a/test-suite/output/inference.out b/test-suite/output/inference.out
index d69baaece..b1952aecf 100644
--- a/test-suite/output/inference.out
+++ b/test-suite/output/inference.out
@@ -4,8 +4,6 @@ fun e : option L => match e with
| None => None
end
: option L -> option L
-
-P is not universe polymorphic
fun (m n p : nat) (H : S m <= S n + p) => le_S_n m (n + p) H
: forall m n p : nat, S m <= S n + p -> m <= n + p
fun n : nat => let x := A n in ?y ?y0:T n
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-23 15:41:27 +0000