From f77b88a498f7e64bc35ade6fa74a00c2550bdf7f Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sat, 20 Jan 2018 22:59:48 +0100 Subject: 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. --- pretyping/tacred.ml | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) (limited to 'pretyping/tacred.ml') diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index 5a522e06a..f682143f8 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -60,9 +60,7 @@ let value_of_evaluable_ref env evref u = match evref with | EvalConstRef con -> let u = Unsafe.to_instance u in - EConstr.of_constr (try constant_value_in env (con,u) - with NotEvaluableConst IsProj -> - raise (Invalid_argument "value_of_evaluable_ref")) + EConstr.of_constr (constant_value_in env (con, u)) | EvalVarRef id -> env |> lookup_named id |> NamedDecl.get_value |> Option.get let evaluable_of_global_reference env = function -- cgit v1.2.3