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 /pretyping/tacred.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 'pretyping/tacred.ml')
| -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 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 |