aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/tacred.ml
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping/tacred.ml')
-rw-r--r--pretyping/tacred.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index bb89756b3..c4c9894cb 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -80,7 +80,7 @@ let reference_opt_value sigma env = function
v
| EvalRel n ->
let (_,v,_) = lookup_rel n env in
- option_map (lift n) v
+ Option.map (lift n) v
| EvalEvar ev -> Evd.existential_opt_value sigma ev
exception NotEvaluable