diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/tacred.ml | 4 |
1 files changed, 1 insertions, 3 deletions
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index 5a522e06a5..f682143f81 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 |