diff options
Diffstat (limited to 'kernel/environ.mli')
| -rw-r--r-- | kernel/environ.mli | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/kernel/environ.mli b/kernel/environ.mli index 520389954..7ce1cea27 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -136,6 +136,7 @@ val evaluable_constant : constant -> env -> bool (** New-style polymorphism *) val polymorphic_constant : constant -> env -> bool val polymorphic_pconstant : pconstant -> env -> bool +val type_in_type_constant : constant -> env -> bool (** Old-style polymorphism *) val template_polymorphic_constant : constant -> env -> bool @@ -183,6 +184,7 @@ val lookup_mind : mutual_inductive -> env -> mutual_inductive_body (** New-style polymorphism *) val polymorphic_ind : inductive -> env -> bool val polymorphic_pind : pinductive -> env -> bool +val type_in_type_ind : inductive -> env -> bool (** Old-style polymorphism *) val template_polymorphic_ind : inductive -> env -> bool |