diff options
Diffstat (limited to 'library')
| -rw-r--r-- | library/declare.ml | 4 | ||||
| -rw-r--r-- | library/declaremods.ml | 2 | ||||
| -rw-r--r-- | library/impargs.ml | 4 | ||||
| -rw-r--r-- | library/lib.ml | 4 | ||||
| -rw-r--r-- | library/libobject.ml | 4 | ||||
| -rw-r--r-- | library/library.ml | 6 |
6 files changed, 12 insertions, 12 deletions
diff --git a/library/declare.ml b/library/declare.ml index 6e9835487..65d08dd81 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -92,7 +92,7 @@ let cache_variable ((sp,_),o) = | SectionLocalDef (c,t,opaq) -> let cst = Global.push_named_def (id,c,t) in let (_,bd,ty) = Global.lookup_named id in - CheckedSectionLocalDef (out_some bd,ty,cst,opaq) in + CheckedSectionLocalDef (Option.get bd,ty,cst,opaq) in Nametab.push (Nametab.Until 1) (restrict_path 0 sp) (VarRef id); add_section_variable id; Dischargedhypsmap.set_discharged_hyps sp []; @@ -200,7 +200,7 @@ let hcons_constant_declaration = function let (hcons1_constr,_) = hcons_constr (hcons_names()) in DefinitionEntry { const_entry_body = hcons1_constr ce.const_entry_body; - const_entry_type = option_map hcons1_constr ce.const_entry_type; + const_entry_type = Option.map hcons1_constr ce.const_entry_type; const_entry_opaque = ce.const_entry_opaque; const_entry_boxed = ce.const_entry_boxed } | cd -> cd diff --git a/library/declaremods.ml b/library/declaremods.ml index 8bfc7ac85..6a73943b9 100644 --- a/library/declaremods.ml +++ b/library/declaremods.ml @@ -579,7 +579,7 @@ let register_library dir cenv objs digest = let msid,substitute,keep = objs in let substobjs = empty_subst, [], msid, substitute in let substituted = subst_substobjs dir mp substobjs in - let objects = option_map (fun seg -> seg@keep) substituted in + let objects = Option.map (fun seg -> seg@keep) substituted in let modobjs = substobjs, objects in Hashtbl.add library_cache dir modobjs; modobjs diff --git a/library/impargs.ml b/library/impargs.ml index 3085b00c0..479936c88 100644 --- a/library/impargs.ml +++ b/library/impargs.ml @@ -259,8 +259,8 @@ let compute_manual_implicits flags ref l = with Not_found -> l, None in let imps' = merge (k+1) l' imps in - let m = option_map (set_maximality imps') m in - option_map (set_implicit id imp) m :: imps' + let m = Option.map (set_maximality imps') m in + Option.map (set_implicit id imp) m :: imps' | (Anonymous,_imp)::imps -> None :: merge (k+1) l imps | [] when l = [] -> [] diff --git a/library/lib.ml b/library/lib.ml index 71494311e..50bef5a5d 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -513,7 +513,7 @@ let open_section id = let discharge_item ((sp,_ as oname),e) = match e with | Leaf lobj -> - option_map (fun o -> (basename sp,o)) (discharge_object (oname,lobj)) + Option.map (fun o -> (basename sp,o)) (discharge_object (oname,lobj)) | FrozenState _ -> None | ClosedSection _ | ClosedModtype _ | ClosedModule _ -> None | OpenedSection _ | OpenedModtype _ | OpenedModule _ | CompilingLibrary _ -> @@ -539,7 +539,7 @@ let close_section id = if !Options.xml_export then !xml_close_section id; let newdecls = List.map discharge_item secdecls in Summary.section_unfreeze_summaries fs; - List.iter (option_iter (fun (id,o) -> add_discharged_leaf id o)) newdecls; + List.iter (Option.iter (fun (id,o) -> add_discharged_leaf id o)) newdecls; Cooking.clear_cooking_sharing (); Nametab.push_dir (Nametab.Until 1) full_olddir (DirClosedSection full_olddir) diff --git a/library/libobject.ml b/library/libobject.ml index 46cc55361..7c74d402b 100644 --- a/library/libobject.ml +++ b/library/libobject.ml @@ -112,7 +112,7 @@ let declare_object odecl = anomaly "somehow we got the wrong dynamic object in the classifyfun" and discharge (oname,lobj) = if Dyn.tag lobj = na then - option_map infun (odecl.discharge_function (oname,outfun lobj)) + Option.map infun (odecl.discharge_function (oname,outfun lobj)) else anomaly "somehow we got the wrong dynamic object in the dischargefun" and rebuild lobj = @@ -120,7 +120,7 @@ let declare_object odecl = else anomaly "somehow we got the wrong dynamic object in the rebuildfun" and exporter lobj = if Dyn.tag lobj = na then - option_map infun (odecl.export_function (outfun lobj)) + Option.map infun (odecl.export_function (outfun lobj)) else anomaly "somehow we got the wrong dynamic object in the exportfun" diff --git a/library/library.ml b/library/library.ml index 70eac95ae..ced150f7b 100644 --- a/library/library.ml +++ b/library/library.ml @@ -496,7 +496,7 @@ let register_library (dir,m) = (* [needed] is the ordered list of libraries not already loaded *) let cache_require (_,(needed,modl,export)) = List.iter register_library needed; - option_iter (fun exp -> open_libraries exp (List.map find_library modl)) + Option.iter (fun exp -> open_libraries exp (List.map find_library modl)) export let load_require _ (_,(needed,modl,_)) = @@ -530,7 +530,7 @@ let require_library qidl export = let modrefl = List.map fst modrefl in if Lib.is_modtype () || Lib.is_module () then begin add_anonymous_leaf (in_require (needed,modrefl,None)); - option_iter (fun exp -> + Option.iter (fun exp -> List.iter (fun dir -> add_anonymous_leaf (in_import(dir,exp))) modrefl) export end @@ -544,7 +544,7 @@ let require_library_from_file idopt file export = let needed = List.rev needed in if Lib.is_modtype () || Lib.is_module () then begin add_anonymous_leaf (in_require (needed,[modref],None)); - option_iter (fun exp -> add_anonymous_leaf (in_import (modref,exp))) + Option.iter (fun exp -> add_anonymous_leaf (in_import (modref,exp))) export end else |