diff options
Diffstat (limited to 'contrib/extraction')
| -rw-r--r-- | contrib/extraction/extract_env.ml | 16 | ||||
| -rw-r--r-- | contrib/extraction/extraction.ml | 4 | ||||
| -rw-r--r-- | contrib/extraction/modutil.ml | 10 | ||||
| -rw-r--r-- | contrib/extraction/ocaml.ml | 2 |
4 files changed, 16 insertions, 16 deletions
diff --git a/contrib/extraction/extract_env.ml b/contrib/extraction/extract_env.ml index b6367d98a2..2aca56f9bb 100644 --- a/contrib/extraction/extract_env.ml +++ b/contrib/extraction/extract_env.ml @@ -241,7 +241,7 @@ and extract_meb env mpo all = function and extract_module env mp all mb = (* [mb.mod_expr <> None ], since we look at modules from outside. *) (* Example of module with empty [mod_expr] is X inside a Module F [X:SIG]. *) - let meb = out_some mb.mod_expr in + let meb = Option.get mb.mod_expr in let mtb = match mb.mod_user_type with None -> mb.mod_type | Some mt -> mt in (* Because of the "with" construct, the module type can be [MTBsig] with *) (* a msid different from the one of the module. Here is the patch. *) @@ -282,7 +282,7 @@ let mono_filename f = Filename.chop_suffix f d.file_suffix else f in - Some (f^d.file_suffix), option_map ((^) f) d.sig_suffix, id_of_string f + Some (f^d.file_suffix), Option.map ((^) f) d.sig_suffix, id_of_string f (* Builds a suitable filename from a module id *) @@ -290,7 +290,7 @@ let module_filename m = let d = descr () in let f = if d.capital_file then String.capitalize else String.uncapitalize in let fn = f (string_of_id m) in - Some (fn^d.file_suffix), option_map ((^) fn) d.sig_suffix, m + Some (fn^d.file_suffix), Option.map ((^) fn) d.sig_suffix, m (*s Extraction of one decl to stdout. *) @@ -317,7 +317,7 @@ let print_structure_to_file (fn,si,mo) struc = else struct_ast_search (function MLmagic _ -> true | _ -> false) struc } in (* print the implementation *) - let cout = option_map open_out fn in + let cout = Option.map open_out fn in let ft = match cout with | None -> !Pp_control.std_ft | Some cout -> Pp_control.with_output_to cout in @@ -330,13 +330,13 @@ let print_structure_to_file (fn,si,mo) struc = reset_renaming_tables OnlyLocal; end; msg_with ft (d.pp_struct struc); - option_iter close_out cout; + Option.iter close_out cout; with e -> - option_iter close_out cout; raise e + Option.iter close_out cout; raise e end; - option_iter info_file fn; + Option.iter info_file fn; (* print the signature *) - option_iter + Option.iter (fun si -> let cout = open_out si in let ft = Pp_control.with_output_to cout in diff --git a/contrib/extraction/extraction.ml b/contrib/extraction/extraction.ml index 77067b2b4c..27687ae1c3 100644 --- a/contrib/extraction/extraction.ml +++ b/contrib/extraction/extraction.ml @@ -310,7 +310,7 @@ and extract_ind env kn = (* kn is supposed to be in long form *) with Not_found -> (* First, if this inductive is aliased via a Module, *) (* we process the original inductive. *) - option_iter (fun kn -> ignore (extract_ind env kn)) mib.mind_equiv; + Option.iter (fun kn -> ignore (extract_ind env kn)) mib.mind_equiv; (* Everything concerning parameters. *) (* We do that first, since they are common to all the [mib]. *) let mip0 = mib.mind_packets.(0) in @@ -413,7 +413,7 @@ and extract_ind env kn = (* kn is supposed to be in long form *) (Inductive.type_of_inductive env (mib,mip0)) in List.iter - (option_iter + (Option.iter (fun kn -> if Cset.mem kn !projs then add_projection n kn)) (lookup_projections ip) with Not_found -> () diff --git a/contrib/extraction/modutil.ml b/contrib/extraction/modutil.ml index 760f76c9a3..79ba0ebc5e 100644 --- a/contrib/extraction/modutil.ml +++ b/contrib/extraction/modutil.ml @@ -39,9 +39,9 @@ let add_structure mp msb env = let rec subst_module sub mb = let mtb' = Modops.subst_modtype sub mb.mod_type - and meb' = option_smartmap (subst_meb sub) mb.mod_expr - and mtb'' = option_smartmap (Modops.subst_modtype sub) mb.mod_user_type - and mpo' = option_smartmap (subst_mp sub) mb.mod_equiv in + and meb' = Option.smartmap (subst_meb sub) mb.mod_expr + and mtb'' = Option.smartmap (Modops.subst_modtype sub) mb.mod_user_type + and mpo' = Option.smartmap (subst_mp sub) mb.mod_equiv in if (mtb'==mb.mod_type) && (meb'==mb.mod_expr) && (mtb''==mb.mod_user_type) && (mpo'==mb.mod_equiv) then mb @@ -170,7 +170,7 @@ let decl_iter_references do_term do_cons do_type = let spec_iter_references do_term do_cons do_type = function | Sind (kn,ind) -> ind_iter_references do_term do_cons do_type kn ind - | Stype (r,_,ot) -> do_type r; option_iter (type_iter_references do_type) ot + | Stype (r,_,ot) -> do_type r; Option.iter (type_iter_references do_type) ot | Sval (r,t) -> do_term r; type_iter_references do_type t let struct_iter_references do_term do_cons do_type = @@ -241,7 +241,7 @@ let spec_type_search f = function | Sind (_,{ind_packets=p}) -> Array.iter (fun {ip_types=v} -> Array.iter (List.iter (type_search f)) v) p - | Stype (_,_,ot) -> option_iter (type_search f) ot + | Stype (_,_,ot) -> Option.iter (type_search f) ot | Sval (_,u) -> type_search f u let struct_type_search f s = diff --git a/contrib/extraction/ocaml.ml b/contrib/extraction/ocaml.ml index f3df9230d0..8ba07ab0b7 100644 --- a/contrib/extraction/ocaml.ml +++ b/contrib/extraction/ocaml.ml @@ -574,7 +574,7 @@ and pp_module_type ol = function str "functor (" ++ name ++ str ":" ++ typ ++ str ") ->" ++ fnl () ++ def | MTsig (msid, sign) -> let tvm = top_visible_mp () in - option_iter (fun l -> add_subst msid (MPdot (tvm, l))) ol; + Option.iter (fun l -> add_subst msid (MPdot (tvm, l))) ol; let mp = MPself msid in push_visible mp; let l = map_succeed pp_specif sign in |