@@ -21,7 +21,7 @@ eq_refl : forall {A : Type} {x : A}, x = x
21
21
eq_refl is template universe polymorphic
22
22
Arguments eq_refl {A}%_type_scope {x}, [_] _
23
23
Expands to: Constructor Corelib.Init.Logic.eq_refl
24
- Declared in library Corelib.Init.Logic, line 382 , characters 4-11
24
+ Declared in library Corelib.Init.Logic, line 378 , characters 4-11
25
25
eq_refl : forall {A : Type} {x : A}, x = x
26
26
27
27
When applied to no arguments:
@@ -63,7 +63,7 @@ comparison : Set
63
63
64
64
comparison is not universe polymorphic
65
65
Expands to: Inductive Corelib.Init.Datatypes.comparison
66
- Declared in library Corelib.Init.Datatypes, line 367 , characters 10-20
66
+ Declared in library Corelib.Init.Datatypes, line 360 , characters 10-20
67
67
Inductive comparison : Set :=
68
68
Eq : comparison | Lt : comparison | Gt : comparison.
69
69
bar : foo
@@ -84,15 +84,15 @@ Arguments bar {x}
84
84
Module Corelib.Init.Peano
85
85
Notation sym_eq := eq_sym
86
86
Expands to: Notation Corelib.Init.Logic.sym_eq
87
- Declared in library Corelib.Init.Logic, line 760 , characters 0-45
87
+ Declared in library Corelib.Init.Logic, line 797 , characters 0-45
88
88
89
89
eq_sym : forall [A : Type] [x y : A], x = y -> y = x
90
90
91
91
eq_sym is not universe polymorphic
92
92
Arguments eq_sym [A]%_type_scope [x y] _
93
93
eq_sym is transparent
94
94
Expands to: Constant Corelib.Init.Logic.eq_sym
95
- Declared in library Corelib.Init.Logic, line 422 , characters 12-18
95
+ Declared in library Corelib.Init.Logic, line 440 , characters 12-18
96
96
Inductive eq (A : Type) (x : A) : A -> Prop := eq_refl : x = x.
97
97
98
98
Arguments eq {A}%_type_scope x _
@@ -115,14 +115,14 @@ Alias.eq is template universe polymorphic
115
115
Arguments Alias.eq {A}%_type_scope x _
116
116
Expands to: Inductive PrintInfos.Alias.eq (syntactically equal to
117
117
Corelib.Init.Logic.eq)
118
- Declared in library Corelib.Init.Logic, line 381 , characters 10-12
118
+ Declared in library Corelib.Init.Logic, line 377 , characters 10-12
119
119
Alias.eq_refl : forall {A : Type} {x : A}, x = x
120
120
121
121
Alias.eq_refl is template universe polymorphic
122
122
Arguments Alias.eq_refl {A}%_type_scope {x}, [_] _
123
123
Expands to: Constructor PrintInfos.Alias.eq_refl (syntactically equal to
124
124
Corelib.Init.Logic.eq_refl)
125
- Declared in library Corelib.Init.Logic, line 382 , characters 4-11
125
+ Declared in library Corelib.Init.Logic, line 378 , characters 4-11
126
126
Alias.eq_ind :
127
127
forall [A : Type] (x : A) (P : A -> Prop), P x -> forall y : A, x = y -> P y
128
128
@@ -132,7 +132,7 @@ Arguments Alias.eq_ind [A]%_type_scope x P%_function_scope eq_refl y e
132
132
Alias.eq_ind is transparent
133
133
Expands to: Constant PrintInfos.Alias.eq_ind (syntactically equal to
134
134
Corelib.Init.Logic.eq_ind)
135
- Declared in library Corelib.Init.Logic, line 381 , characters 0-115
135
+ Declared in library Corelib.Init.Logic, line 377 , characters 0-115
136
136
fst : forall A B : Type, prod A B -> A
137
137
138
138
fst is not universe polymorphic
0 commit comments