diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2018-01-20 22:59:48 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2018-01-20 23:41:45 +0100 |
| commit | f77b88a498f7e64bc35ade6fa74a00c2550bdf7f (patch) | |
| tree | a8a99714d5bb73cdb24be830097e88bb8dfba2bb /kernel/environ.mli | |
| parent | 9aa2464375c1515aa64df7dc910e2f324e34c82f (diff) | |
Remove dead code in Environ.
The constant_value function was actually not behaving the same as
constant_value_in w.r.t. projections. The former was not used, and
the only place that used the latter was in Tacred and was statically
insensitive to the use of projections.
Diffstat (limited to 'kernel/environ.mli')
| -rw-r--r-- | kernel/environ.mli | 4 |
1 files changed, 1 insertions, 3 deletions
diff --git a/kernel/environ.mli b/kernel/environ.mli index 7cc541258..69d811a64 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -146,13 +146,11 @@ val type_in_type_constant : Constant.t -> env -> bool body and [NotEvaluableConst IsProj] if [c] is a projection and [Not_found] if it does not exist in [env] *) -type const_evaluation_result = NoBody | Opaque | IsProj +type const_evaluation_result = NoBody | Opaque exception NotEvaluableConst of const_evaluation_result -val constant_value : env -> Constant.t puniverses -> constr constrained val constant_type : env -> Constant.t puniverses -> types constrained -val constant_opt_value : env -> Constant.t puniverses -> (constr * Univ.Constraint.t) option val constant_value_and_type : env -> Constant.t puniverses -> constr option * types * Univ.Constraint.t (** The universe context associated to the constant, empty if not |