diff options
| author | Pierre-Marie Pédrot | 2018-01-20 22:59:48 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-01-20 23:41:45 +0100 |
| commit | f77b88a498f7e64bc35ade6fa74a00c2550bdf7f (patch) | |
| tree | a8a99714d5bb73cdb24be830097e88bb8dfba2bb /kernel/environ.ml | |
| 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.ml')
| -rw-r--r-- | kernel/environ.ml | 23 |
1 files changed, 1 insertions, 22 deletions
diff --git a/kernel/environ.ml b/kernel/environ.ml index 3c86129fed..d967eeadf9 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 |