aboutsummaryrefslogtreecommitdiffhomepage
path: root/contrib/correctness/pmisc.ml
diff options
context:
space:
mode:
Diffstat (limited to 'contrib/correctness/pmisc.ml')
-rw-r--r--contrib/correctness/pmisc.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/contrib/correctness/pmisc.ml b/contrib/correctness/pmisc.ml
index 6b14fd304..23c1028a4 100644
--- a/contrib/correctness/pmisc.ml
+++ b/contrib/correctness/pmisc.ml
@@ -216,7 +216,7 @@ let rec type_v_knsubst s = function
and type_c_knsubst s ((id,v),e,pl,q) =
((id, type_v_knsubst s v), e,
List.map (fun p -> { p with p_value = subst_mps s p.p_value }) pl,
- option_map (fun q -> { q with a_value = subst_mps s q.a_value }) q)
+ Option.map (fun q -> { q with a_value = subst_mps s q.a_value }) q)
and binder_knsubst s (id,b) =
(id, match b with BindType v -> BindType (type_v_knsubst s v) | _ -> b)