diff options
Diffstat (limited to 'pretyping/tacred.ml')
| -rw-r--r-- | pretyping/tacred.ml | 5 |
1 files changed, 0 insertions, 5 deletions
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index b405afa93..a32d54b5e 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -59,11 +59,6 @@ let value_of_evaluable_ref env evref u = raise (Invalid_argument "value_of_evaluable_ref")) | EvalVarRef id -> Option.get (pi2 (lookup_named id env)) -let constr_of_evaluable_ref evref u = - match evref with - | EvalConstRef con -> mkConstU (con,u) - | EvalVarRef id -> mkVar id - let evaluable_of_global_reference env = function | ConstRef cst when is_evaluable_const env cst -> EvalConstRef cst | VarRef id when is_evaluable_var env id -> EvalVarRef id |