diff options
Diffstat (limited to 'kernel/sign.ml')
| -rw-r--r-- | kernel/sign.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/kernel/sign.ml b/kernel/sign.ml index c2b4eca75..79619b48f 100644 --- a/kernel/sign.ml +++ b/kernel/sign.ml @@ -73,7 +73,7 @@ let fold_rel_context_reverse f ~init:x l = List.fold_left f x l let map_context f l = let map_decl (n, body_o, typ as decl) = - let body_o' = option_smartmap f body_o in + let body_o' = Option.smartmap f body_o in let typ' = f typ in if body_o' == body_o && typ' == typ then decl else (n, body_o', typ') @@ -83,8 +83,8 @@ let map_context f l = let map_rel_context = map_context let map_named_context = map_context -let iter_rel_context f = List.iter (fun (_,b,t) -> f t; option_iter f b) -let iter_named_context f = List.iter (fun (_,b,t) -> f t; option_iter f b) +let iter_rel_context f = List.iter (fun (_,b,t) -> f t; Option.iter f b) +let iter_named_context f = List.iter (fun (_,b,t) -> f t; Option.iter f b) (* Push named declarations on top of a rel context *) (* Bizarre. Should be avoided. *) @@ -92,7 +92,7 @@ let push_named_to_rel_context hyps ctxt = let rec push = function | (id,b,t) :: l -> let s, hyps = push l in - let d = (Name id, option_map (subst_vars s) b, subst_vars s t) in + let d = (Name id, Option.map (subst_vars s) b, subst_vars s t) in id::s, d::hyps | [] -> [],[] in let s, hyps = push hyps in |