diff options
| author |  Matthieu Sozeau <mattam@mattam.org> | 2013-10-28 14:08:46 +0100 |
|---|---|---|
| committer | Matthieu Sozeau <mattam@mattam.org> | 2014-05-06 09:58:54 +0200 |
| commit | 001ff72b2c17fb7b2fcaefa2555c115f0d909a03 (patch) | |
| tree | 9e83ae395173699a7c5b6f00648c4336bedb7afd /kernel/environ.mli | |
| parent | 84cbc09bd1400f732a6c70e8a840e4c13d018478 (diff) | |
Initial work on reintroducing old-style polymorphism for compatibility (the stdlib does not compile entirely).
Diffstat (limited to 'kernel/environ.mli')
| -rw-r--r-- | kernel/environ.mli | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/kernel/environ.mli b/kernel/environ.mli index fb5d79718..330d9c277 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -140,12 +140,12 @@ 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 -> types constrained -val constant_type_in_ctx : env -> constant -> types Univ.in_universe_context +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 -> - types option * constr * Univ.constraints + constr option * constant_type * Univ.constraints (** The universe context associated to the constant, empty if not polymorphic *) val constant_context : env -> constant -> Univ.universe_context @@ -154,7 +154,7 @@ val constant_context : env -> constant -> Univ.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 -> types +val constant_type_in : env -> constant puniverses -> constant_type val constant_opt_value_in : env -> constant puniverses -> constr option |