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 | |
| 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')
| -rw-r--r-- | kernel/environ.ml | 23 | ||||
| -rw-r--r-- | kernel/environ.mli | 4 |
2 files changed, 2 insertions, 25 deletions
diff --git a/kernel/environ.ml b/kernel/environ.ml index 3c86129fe..d967eeadf 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -251,31 +251,10 @@ let constant_context env kn = | Monomorphic_const _ -> Univ.AUContext.empty | Polymorphic_const ctx -> ctx -type const_evaluation_result = NoBody | Opaque | IsProj +type const_evaluation_result = NoBody | Opaque exception NotEvaluableConst of const_evaluation_result -let constant_value env (kn,u) = - let cb = lookup_constant kn env in - if cb.const_proj = None then - match cb.const_body with - | Def l_body -> - begin - match cb.const_universes with - | Monomorphic_const _ -> - (Mod_subst.force_constr l_body, Univ.Constraint.empty) - | Polymorphic_const _ -> - let csts = constraints_of cb u in - (subst_instance_constr u (Mod_subst.force_constr l_body), csts) - end - | OpaqueDef _ -> raise (NotEvaluableConst Opaque) - | Undef _ -> raise (NotEvaluableConst NoBody) - else raise (NotEvaluableConst IsProj) - -let constant_opt_value env cst = - try Some (constant_value env cst) - with NotEvaluableConst _ -> None - let constant_value_and_type env (kn, u) = let cb = lookup_constant kn env in if Declareops.constant_is_polymorphic cb then 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 |