diff options
Diffstat (limited to 'kernel/environ.mli')
| -rw-r--r-- | kernel/environ.mli | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/kernel/environ.mli b/kernel/environ.mli index d885ddd56..28eecc7ef 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -144,7 +144,6 @@ 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_in_ctx : env -> constant -> constant_type Univ.in_universe_context val constant_opt_value : env -> constant puniverses -> (constr * Univ.constraints) option val constant_value_and_type : env -> constant puniverses -> |