diff options
Diffstat (limited to 'kernel/environ.mli')
| -rw-r--r-- | kernel/environ.mli | 10 |
1 files changed, 3 insertions, 7 deletions
diff --git a/kernel/environ.mli b/kernel/environ.mli index cd7a9d2791..377c61de2c 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -139,10 +139,6 @@ 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 -val template_polymorphic_pconstant : pconstant -> env -> bool - (** {6 ... } *) (** [constant_value env c] raises [NotEvaluableConst Opaque] if [c] is opaque and [NotEvaluableConst NoBody] if it has no @@ -153,11 +149,11 @@ type const_evaluation_result = NoBody | Opaque | IsProj exception NotEvaluableConst of const_evaluation_result val constant_value : env -> constant puniverses -> constr constrained -val constant_type : env -> constant puniverses -> constant_type constrained +val constant_type : env -> constant puniverses -> types constrained val constant_opt_value : env -> constant puniverses -> (constr * Univ.constraints) option val constant_value_and_type : env -> constant puniverses -> - constr option * constant_type * Univ.constraints + constr option * types * Univ.constraints (** The universe context associated to the constant, empty if not polymorphic *) val constant_context : env -> constant -> Univ.abstract_universe_context @@ -166,7 +162,7 @@ val constant_context : env -> constant -> Univ.abstract_universe_context already contains the constraints corresponding to the constant application. *) val constant_value_in : env -> constant puniverses -> constr -val constant_type_in : env -> constant puniverses -> constant_type +val constant_type_in : env -> constant puniverses -> types val constant_opt_value_in : env -> constant puniverses -> constr option (** {6 Primitive projections} *) |