diff options
93 files changed, 620 insertions, 469 deletions
diff --git a/Makefile.common b/Makefile.common index 22466fe10..2367c14ea 100644 --- a/Makefile.common +++ b/Makefile.common @@ -70,7 +70,7 @@ LIBREP:=\ lib/hashcons.cmo lib/dyn.cmo lib/system.cmo lib/options.cmo \ lib/bstack.cmo lib/edit.cmo lib/gset.cmo lib/gmap.cmo \ lib/tlm.cmo lib/gmapl.cmo lib/profile.cmo lib/explore.cmo \ - lib/predicate.cmo lib/rtree.cmo lib/heap.cmo + lib/predicate.cmo lib/rtree.cmo lib/heap.cmo lib/option.cmo # Rem: Cygwin already uses variable LIB BYTERUN:=\ @@ -349,7 +349,7 @@ MINICOQCMO:=$(CONFIG) $(LIBREP) $(KERNEL) \ GRAMMARNEEDEDCMO:=\ lib/pp_control.cmo lib/pp.cmo lib/compat.cmo lib/util.cmo lib/bigint.cmo \ lib/dyn.cmo lib/options.cmo lib/hashcons.cmo lib/predicate.cmo \ - lib/rtree.cmo \ + lib/rtree.cmo lib/option.cmo \ kernel/names.cmo kernel/univ.cmo \ kernel/esubst.cmo kernel/term.cmo kernel/mod_subst.cmo kernel/sign.cmo \ kernel/cbytecodes.cmo kernel/copcodes.cmo kernel/cemitcodes.cmo \ 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) diff --git a/contrib/correctness/pmonad.ml b/contrib/correctness/pmonad.ml index 1a4ddbc2c..a341ba2ba 100644 --- a/contrib/correctness/pmonad.ml +++ b/contrib/correctness/pmonad.ml @@ -76,9 +76,9 @@ let rec abstract_post ren env (e,q) = let after_id id = id_of_string ((string_of_id id) ^ "'") in let (_,go) = Peffect.get_repr e in let al = List.map (fun id -> (id,after_id id)) go in - let q = option_map (named_app (subst_in_constr al)) q in + let q = Option.map (named_app (subst_in_constr al)) q in let tgo = List.map (fun (id,aid) -> (aid, trad_type_in_env ren env id)) al in - option_map (named_app (abstract tgo)) q + Option.map (named_app (abstract tgo)) q (* Translation of effects types in cic types. * @@ -365,7 +365,7 @@ let make_app env ren args ren' (tf,cf) ((bl,cb),s,capp) c = @(eq_phi ren'' env s svi tf) @(List.map (fun c -> CC_hole c) holes)) in - let qapp' = option_map (named_app (subst_in_constr svi)) qapp in + let qapp' = Option.map (named_app (subst_in_constr svi)) qapp in let t = make_let_in ren'' env fe [] (current_vars ren''' outf,qapp') (res,tyres) (t,ty) diff --git a/contrib/correctness/psyntax.ml4 b/contrib/correctness/psyntax.ml4 index 72b609b24..bb9a355c3 100644 --- a/contrib/correctness/psyntax.ml4 +++ b/contrib/correctness/psyntax.ml4 @@ -787,7 +787,7 @@ END VERNAC COMMAND EXTEND Correctness [ "Correctness" preident(str) program(pgm) then_tac(tac) ] - -> [ Ptactic.correctness str pgm (option_map Tacinterp.interp tac) ] + -> [ Ptactic.correctness str pgm (Option.map Tacinterp.interp tac) ] END (* Show Programs *) diff --git a/contrib/correctness/putil.ml b/contrib/correctness/putil.ml index 46cd12403..e4bac65f4 100644 --- a/contrib/correctness/putil.ml +++ b/contrib/correctness/putil.ml @@ -41,7 +41,7 @@ let anonymous x = { a_name = Anonymous; a_value = x } let anonymous_pre b x = { p_assert = b; p_name = Anonymous; p_value = x } let force_name f x = - option_map (fun q -> { a_name = Name (f q.a_name); a_value = q.a_value }) x + Option.map (fun q -> { a_name = Name (f q.a_name); a_value = q.a_value }) x let force_post_name x = force_name post_name x @@ -143,7 +143,7 @@ let rec type_c_subst s ((id,t),e,p,q) = let s' = s @ List.map (fun (x,x') -> (at_id x "", at_id x' "")) s in (id, type_v_subst s t), Peffect.subst s e, List.map (pre_app (subst_in_constr s)) p, - option_map (post_app (subst_in_constr s')) q + Option.map (post_app (subst_in_constr s')) q and type_v_subst s = function Ref v -> Ref (type_v_subst s v) @@ -160,7 +160,7 @@ and binder_subst s = function let rec type_c_rsubst s ((id,t),e,p,q) = (id, type_v_rsubst s t), e, List.map (pre_app (real_subst_in_constr s)) p, - option_map (post_app (real_subst_in_constr s)) q + Option.map (post_app (real_subst_in_constr s)) q and type_v_rsubst s = function Ref v -> Ref (type_v_rsubst s v) diff --git a/contrib/correctness/pwp.ml b/contrib/correctness/pwp.ml index 70e9eee29..258a46150 100644 --- a/contrib/correctness/pwp.ml +++ b/contrib/correctness/pwp.ml @@ -64,7 +64,7 @@ let update_post env top ef c = let force_post up env top q e = let (res,ef,p,_) = e.info.kappa in let q' = - if up then option_map (named_app (update_post env top ef)) q else q + if up then Option.map (named_app (update_post env top ef)) q else q in let i = { env = e.info.env; kappa = (res,ef,p,q') } in { desc = e.desc; pre = e.pre; post = q'; loc = e.loc; info = i } @@ -260,7 +260,7 @@ and propagate ren p = | Apply (f,l) -> let _,(_,so,ok),(_,_,_,qapp) = effect_app ren env f l in if ok then - let q = option_map (named_app (real_subst_in_constr so)) qapp in + let q = Option.map (named_app (real_subst_in_constr so)) qapp in post_if_none env q p else p @@ -285,7 +285,7 @@ and propagate ren p = None -> Some (anonymous s) | Some i -> Some { a_value = conj i.a_value s; a_name = i.a_name } in - let q = option_map (named_app abstract_unit) q in + let q = Option.map (named_app abstract_unit) q in post_if_none env q p | SApp ([Variable id], [e1;e2]) diff --git a/contrib/extraction/extract_env.ml b/contrib/extraction/extract_env.ml index b6367d98a..2aca56f9b 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 77067b2b4..27687ae1c 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 760f76c9a..79ba0ebc5 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 f3df9230d..8ba07ab0b 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 diff --git a/contrib/first-order/g_ground.ml4 b/contrib/first-order/g_ground.ml4 index e48d47d9d..3ee1db14c 100644 --- a/contrib/first-order/g_ground.ml4 +++ b/contrib/first-order/g_ground.ml4 @@ -98,16 +98,16 @@ let normalize_evaluables= TACTIC EXTEND firstorder [ "firstorder" tactic_opt(t) "using" ne_reference_list(l) ] -> - [ gen_ground_tac true (option_map eval_tactic t) (Ids l) ] + [ gen_ground_tac true (Option.map eval_tactic t) (Ids l) ] | [ "firstorder" tactic_opt(t) "with" ne_preident_list(l) ] -> - [ gen_ground_tac true (option_map eval_tactic t) (Bases l) ] + [ gen_ground_tac true (Option.map eval_tactic t) (Bases l) ] | [ "firstorder" tactic_opt(t) ] -> - [ gen_ground_tac true (option_map eval_tactic t) Void ] + [ gen_ground_tac true (Option.map eval_tactic t) Void ] END TACTIC EXTEND gintuition [ "gintuition" tactic_opt(t) ] -> - [ gen_ground_tac false (option_map eval_tactic t) Void ] + [ gen_ground_tac false (Option.map eval_tactic t) Void ] END diff --git a/contrib/funind/functional_principles_proofs.ml b/contrib/funind/functional_principles_proofs.ml index b10aa782c..45976d6e5 100644 --- a/contrib/funind/functional_principles_proofs.ml +++ b/contrib/funind/functional_principles_proofs.ml @@ -882,7 +882,7 @@ let generate_equation_lemma fnames f fun_num nb_params nb_args rec_args_num = let f_def = Global.lookup_constant (destConst f) in let eq_lhs = mkApp(f,Array.init (nb_params + nb_args) (fun i -> mkRel(nb_params + nb_args - i))) in let f_body = - force (out_some f_def.const_body) + force (Option.get f_def.const_body) in let params,f_body_with_params = decompose_lam_n nb_params f_body in let (_,num),(_,_,bodies) = destFix f_body_with_params in @@ -933,8 +933,8 @@ let do_replace params rec_arg_num rev_args_id f fun_num all_funs g = let equation_lemma = try let finfos = find_Function_infos (destConst f) in - mkConst (out_some finfos.equation_lemma) - with (Not_found | Failure "out_some" as e) -> + mkConst (Option.get finfos.equation_lemma) + with (Not_found | Option.IsNone as e) -> let f_id = id_of_label (con_label (destConst f)) in (*i The next call to mk_equation_id is valid since we will construct the lemma Ensures by: obvious @@ -943,7 +943,7 @@ let do_replace params rec_arg_num rev_args_id f fun_num all_funs g = generate_equation_lemma all_funs f fun_num (List.length params) (List.length rev_args_id) rec_arg_num; let _ = match e with - | Failure "out_some" -> + | Option.IsNone -> let finfos = find_Function_infos (destConst f) in update_Function {finfos with diff --git a/contrib/funind/functional_principles_types.ml b/contrib/funind/functional_principles_types.ml index cb804f6f2..72f930b0a 100644 --- a/contrib/funind/functional_principles_types.ml +++ b/contrib/funind/functional_principles_types.ml @@ -115,7 +115,7 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type = it_mkProd_or_LetIn ~init: (it_mkProd_or_LetIn - ~init:(option_fold_right + ~init:(Option.fold_right mkProd_or_LetIn princ_type_info.indarg princ_type_info.concl @@ -564,9 +564,9 @@ let make_scheme (fas : (constant*Rawterm.rawsort) list) : Entries.definition_ent let opacity = let finfos = find_Function_infos this_block_funs.(0) in try - let equation = out_some finfos.equation_lemma in + let equation = Option.get finfos.equation_lemma in (Global.lookup_constant equation).Declarations.const_opaque - with Failure "out_some" -> (* non recursive definition *) + with Option.IsNone -> (* non recursive definition *) false in let const = {const with const_entry_opaque = opacity } in diff --git a/contrib/funind/indfun.ml b/contrib/funind/indfun.ml index 199e01525..3102f1b5d 100644 --- a/contrib/funind/indfun.ml +++ b/contrib/funind/indfun.ml @@ -48,8 +48,8 @@ let functional_induction with_clean c princl pat = | InType -> finfo.rect_lemma in let princ = (* then we get the principle *) - try mkConst (out_some princ_option ) - with Failure "out_some" -> + try mkConst (Option.get princ_option ) + with Option.IsNone -> (*i If there is not default lemma defined then, we cross our finger and try to find a lemma named f_ind (or f_rec, f_rect) i*) @@ -589,21 +589,21 @@ let rec add_args id new_args b = CApp(loc,(pf,add_args id new_args b), List.map (fun (e,o) -> add_args id new_args e,o) bl) | CCases(loc,b_option,cel,cal) -> - CCases(loc,option_map (add_args id new_args) b_option, + CCases(loc,Option.map (add_args id new_args) b_option, List.map (fun (b,(na,b_option)) -> add_args id new_args b, - (na,option_map (add_args id new_args) b_option)) cel, + (na,Option.map (add_args id new_args) b_option)) cel, List.map (fun (loc,cpl,e) -> (loc,cpl,add_args id new_args e)) cal ) | CLetTuple(loc,nal,(na,b_option),b1,b2) -> - CLetTuple(loc,nal,(na,option_map (add_args id new_args) b_option), + CLetTuple(loc,nal,(na,Option.map (add_args id new_args) b_option), add_args id new_args b1, add_args id new_args b2 ) | CIf(loc,b1,(na,b_option),b2,b3) -> CIf(loc,add_args id new_args b1, - (na,option_map (add_args id new_args) b_option), + (na,Option.map (add_args id new_args) b_option), add_args id new_args b2, add_args id new_args b3 ) @@ -722,7 +722,7 @@ let make_graph (f_ref:global_reference) = ) in let rec_id = - match List.nth bl' (out_some n) with + match List.nth bl' (Option.get n) with |(_,Name id) -> id | _ -> anomaly "" in let new_args = diff --git a/contrib/funind/indfun_common.ml b/contrib/funind/indfun_common.ml index 609504ba5..c2372d3ed 100644 --- a/contrib/funind/indfun_common.ml +++ b/contrib/funind/indfun_common.ml @@ -319,12 +319,12 @@ let subst_Function (_,subst,finfos) = in let function_constant' = do_subst_con finfos.function_constant in let graph_ind' = do_subst_ind finfos.graph_ind in - let equation_lemma' = Util.option_smartmap do_subst_con finfos.equation_lemma in - let correctness_lemma' = Util.option_smartmap do_subst_con finfos.correctness_lemma in - let completeness_lemma' = Util.option_smartmap do_subst_con finfos.completeness_lemma in - let rect_lemma' = Util.option_smartmap do_subst_con finfos.rect_lemma in - let rec_lemma' = Util.option_smartmap do_subst_con finfos.rec_lemma in - let prop_lemma' = Util.option_smartmap do_subst_con finfos.prop_lemma in + let equation_lemma' = Option.smartmap do_subst_con finfos.equation_lemma in + let correctness_lemma' = Option.smartmap do_subst_con finfos.correctness_lemma in + let completeness_lemma' = Option.smartmap do_subst_con finfos.completeness_lemma in + let rect_lemma' = Option.smartmap do_subst_con finfos.rect_lemma in + let rec_lemma' = Option.smartmap do_subst_con finfos.rec_lemma in + let prop_lemma' = Option.smartmap do_subst_con finfos.prop_lemma in if function_constant' == finfos.function_constant && graph_ind' == finfos.graph_ind && equation_lemma' == finfos.equation_lemma && @@ -354,12 +354,12 @@ let export_Function infos = Some infos let discharge_Function (_,finfos) = let function_constant' = Lib.discharge_con finfos.function_constant and graph_ind' = Lib.discharge_inductive finfos.graph_ind - and equation_lemma' = Util.option_smartmap Lib.discharge_con finfos.equation_lemma - and correctness_lemma' = Util.option_smartmap Lib.discharge_con finfos.correctness_lemma - and completeness_lemma' = Util.option_smartmap Lib.discharge_con finfos.completeness_lemma - and rect_lemma' = Util.option_smartmap Lib.discharge_con finfos.rect_lemma - and rec_lemma' = Util.option_smartmap Lib.discharge_con finfos.rec_lemma - and prop_lemma' = Util.option_smartmap Lib.discharge_con finfos.prop_lemma + and equation_lemma' = Option.smartmap Lib.discharge_con finfos.equation_lemma + and correctness_lemma' = Option.smartmap Lib.discharge_con finfos.correctness_lemma + and completeness_lemma' = Option.smartmap Lib.discharge_con finfos.completeness_lemma + and rect_lemma' = Option.smartmap Lib.discharge_con finfos.rect_lemma + and rec_lemma' = Option.smartmap Lib.discharge_con finfos.rec_lemma + and prop_lemma' = Option.smartmap Lib.discharge_con finfos.prop_lemma in if function_constant' == finfos.function_constant && graph_ind' == finfos.graph_ind && @@ -387,12 +387,12 @@ let pr_info f_info = str "function_constant := " ++ Printer.pr_lconstr (mkConst f_info.function_constant)++ fnl () ++ str "function_constant_type := " ++ (try Printer.pr_lconstr (Global.type_of_global (ConstRef f_info.function_constant)) with _ -> mt ()) ++ fnl () ++ - str "equation_lemma := " ++ (Util.option_fold_right (fun v acc -> Printer.pr_lconstr (mkConst v)) f_info.equation_lemma (mt ()) ) ++ fnl () ++ - str "completeness_lemma :=" ++ (Util.option_fold_right (fun v acc -> Printer.pr_lconstr (mkConst v)) f_info.completeness_lemma (mt ()) ) ++ fnl () ++ - str "correctness_lemma := " ++ (Util.option_fold_right (fun v acc -> Printer.pr_lconstr (mkConst v)) f_info.correctness_lemma (mt ()) ) ++ fnl () ++ - str "rect_lemma := " ++ (Util.option_fold_right (fun v acc -> Printer.pr_lconstr (mkConst v)) f_info.rect_lemma (mt ()) ) ++ fnl () ++ - str "rec_lemma := " ++ (Util.option_fold_right (fun v acc -> Printer.pr_lconstr (mkConst v)) f_info.rec_lemma (mt ()) ) ++ fnl () ++ - str "prop_lemma := " ++ (Util.option_fold_right (fun v acc -> Printer.pr_lconstr (mkConst v)) f_info.prop_lemma (mt ()) ) ++ fnl () ++ + str "equation_lemma := " ++ (Option.fold_right (fun v acc -> Printer.pr_lconstr (mkConst v)) f_info.equation_lemma (mt ()) ) ++ fnl () ++ + str "completeness_lemma :=" ++ (Option.fold_right (fun v acc -> Printer.pr_lconstr (mkConst v)) f_info.completeness_lemma (mt ()) ) ++ fnl () ++ + str "correctness_lemma := " ++ (Option.fold_right (fun v acc -> Printer.pr_lconstr (mkConst v)) f_info.correctness_lemma (mt ()) ) ++ fnl () ++ + str "rect_lemma := " ++ (Option.fold_right (fun v acc -> Printer.pr_lconstr (mkConst v)) f_info.rect_lemma (mt ()) ) ++ fnl () ++ + str "rec_lemma := " ++ (Option.fold_right (fun v acc -> Printer.pr_lconstr (mkConst v)) f_info.rec_lemma (mt ()) ) ++ fnl () ++ + str "prop_lemma := " ++ (Option.fold_right (fun v acc -> Printer.pr_lconstr (mkConst v)) f_info.prop_lemma (mt ()) ) ++ fnl () ++ str "graph_ind := " ++ Printer.pr_lconstr (mkInd f_info.graph_ind) ++ fnl () let pr_table tb = diff --git a/contrib/funind/invfun.ml b/contrib/funind/invfun.ml index 6171e8194..dcbefe4a4 100644 --- a/contrib/funind/invfun.ml +++ b/contrib/funind/invfun.ml @@ -665,8 +665,8 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic = if infos.is_general || Rtree.is_infinite graph_def.mind_recargs then let eq_lemma = - try out_some (infos).equation_lemma - with Failure "out_some" -> anomaly "Cannot find equation lemma" + try Option.get (infos).equation_lemma + with Option.IsNone -> anomaly "Cannot find equation lemma" in tclTHENSEQ[ tclMAP h_intro ids; @@ -769,7 +769,7 @@ let derive_correctness make_scheme functional_induction (funs: constant list) (g Array.of_list (List.map (fun entry -> - (entry.Entries.const_entry_body, out_some entry.Entries.const_entry_type ) + (entry.Entries.const_entry_body, Option.get entry.Entries.const_entry_type ) ) (make_scheme (array_map_to_list (fun const -> const,Rawterm.RType None) funs)) ) @@ -960,13 +960,13 @@ let invfun qhyp f = in try let finfos = find_Function_infos f in - let f_correct = mkConst(out_some finfos.correctness_lemma) + let f_correct = mkConst(Option.get finfos.correctness_lemma) and kn = fst finfos.graph_ind in Tactics.try_intros_until (fun hid -> functional_inversion kn hid (mkConst f) f_correct) qhyp with | Not_found -> error "No graph found" - | Failure "out_some" -> error "Cannot use equivalence with graph!" + | Option.IsNone -> error "Cannot use equivalence with graph!" let invfun qhyp f g = @@ -983,23 +983,23 @@ let invfun qhyp f g = try if not (isConst f1) then failwith ""; let finfos = find_Function_infos (destConst f1) in - let f_correct = mkConst(out_some finfos.correctness_lemma) + let f_correct = mkConst(Option.get finfos.correctness_lemma) and kn = fst finfos.graph_ind in functional_inversion kn hid f1 f_correct g - with | Failure "" | Failure "out_some" | Not_found -> + with | Failure "" | Option.IsNone | Not_found -> try let f2,_ = decompose_app args.(2) in if not (isConst f2) then failwith ""; let finfos = find_Function_infos (destConst f2) in - let f_correct = mkConst(out_some finfos.correctness_lemma) + let f_correct = mkConst(Option.get finfos.correctness_lemma) and kn = fst finfos.graph_ind in functional_inversion kn hid f2 f_correct g with | Failure "" -> errorlabstrm "" (str "Hypothesis" ++ Ppconstr.pr_id hid ++ str " must contain at leat one Function") - | Failure "out_some" -> + | Option.IsNone -> if do_observe () then error "Cannot use equivalence with graph for any side of the equality" diff --git a/contrib/funind/rawterm_to_relation.ml b/contrib/funind/rawterm_to_relation.ml index b34a1097a..af0a2addc 100644 --- a/contrib/funind/rawterm_to_relation.ml +++ b/contrib/funind/rawterm_to_relation.ml @@ -368,7 +368,7 @@ let raw_push_named (na,raw_value,raw_typ) env = match na with | Anonymous -> env | Name id -> - let value = Util.option_map (Pretyping.Default.understand Evd.empty env) raw_value in + let value = Option.map (Pretyping.Default.understand Evd.empty env) raw_value in let typ = Pretyping.Default.understand_type Evd.empty env raw_typ in Environ.push_named (id,value,typ) env @@ -398,12 +398,12 @@ let add_pat_variables pat typ env : Environ.env = | Anonymous -> assert false | Name id -> let new_t = substl ctxt t in - let new_v = option_map (substl ctxt) v in + let new_v = Option.map (substl ctxt) v in observe (str "for variable " ++ Ppconstr.pr_id id ++ fnl () ++ str "old type := " ++ Printer.pr_lconstr t ++ fnl () ++ str "new type := " ++ Printer.pr_lconstr new_t ++ fnl () ++ - option_fold_right (fun v _ -> str "old value := " ++ Printer.pr_lconstr v ++ fnl ()) v (mt ()) ++ - option_fold_right (fun v _ -> str "new value := " ++ Printer.pr_lconstr v ++ fnl ()) new_v (mt ()) + Option.fold_right (fun v _ -> str "old value := " ++ Printer.pr_lconstr v ++ fnl ()) v (mt ()) ++ + Option.fold_right (fun v _ -> str "new value := " ++ Printer.pr_lconstr v ++ fnl ()) new_v (mt ()) ); (Environ.push_named (id,new_v,new_t) env,mkVar id::ctxt) ) diff --git a/contrib/funind/rawtermops.ml b/contrib/funind/rawtermops.ml index f9e188dac..e8cce47ad 100644 --- a/contrib/funind/rawtermops.ml +++ b/contrib/funind/rawtermops.ml @@ -157,7 +157,7 @@ let change_vars = let new_mapping = List.fold_left remove_name_from_mapping mapping nal in RLetTuple(loc, nal, - (na, option_map (change_vars mapping) rto), + (na, Option.map (change_vars mapping) rto), change_vars mapping b, change_vars new_mapping e ) @@ -170,7 +170,7 @@ let change_vars = | RIf(loc,b,(na,e_option),lhs,rhs) -> RIf(loc, change_vars mapping b, - (na,option_map (change_vars mapping) e_option), + (na,Option.map (change_vars mapping) e_option), change_vars mapping lhs, change_vars mapping rhs ) @@ -338,11 +338,11 @@ let rec alpha_rt excluded rt = if idmap_is_empty mapping then rto,t,b else let replace = change_vars mapping in - (option_map replace rto, t,replace b) + (Option.map replace rto, t,replace b) in let new_t = alpha_rt new_excluded new_t in let new_b = alpha_rt new_excluded new_b in - let new_rto = option_map (alpha_rt new_excluded) new_rto in + let new_rto = Option.map (alpha_rt new_excluded) new_rto in RLetTuple(loc,new_nal,(na,new_rto),new_t,new_b) | RCases(loc,infos,el,brl) -> let new_el = @@ -351,7 +351,7 @@ let rec alpha_rt excluded rt = RCases(loc,infos,new_el,List.map (alpha_br excluded) brl) | RIf(loc,b,(na,e_o),lhs,rhs) -> RIf(loc,alpha_rt excluded b, - (na,option_map (alpha_rt excluded) e_o), + (na,Option.map (alpha_rt excluded) e_o), alpha_rt excluded lhs, alpha_rt excluded rhs ) @@ -487,7 +487,7 @@ let replace_var_by_term x_id term = | RLetTuple(loc,nal,(na,rto),def,b) -> RLetTuple(loc, nal, - (na,option_map replace_var_by_pattern rto), + (na,Option.map replace_var_by_pattern rto), replace_var_by_pattern def, replace_var_by_pattern b ) @@ -499,7 +499,7 @@ let replace_var_by_term x_id term = ) | RIf(loc,b,(na,e_option),lhs,rhs) -> RIf(loc, replace_var_by_pattern b, - (na,option_map replace_var_by_pattern e_option), + (na,Option.map replace_var_by_pattern e_option), replace_var_by_pattern lhs, replace_var_by_pattern rhs ) @@ -640,7 +640,7 @@ let zeta_normalize = | RLetTuple(loc,nal,(na,rto),def,b) -> RLetTuple(loc, nal, - (na,option_map zeta_normalize_term rto), + (na,Option.map zeta_normalize_term rto), zeta_normalize_term def, zeta_normalize_term b ) @@ -652,7 +652,7 @@ let zeta_normalize = ) | RIf(loc,b,(na,e_option),lhs,rhs) -> RIf(loc, zeta_normalize_term b, - (na,option_map zeta_normalize_term e_option), + (na,Option.map zeta_normalize_term e_option), zeta_normalize_term lhs, zeta_normalize_term rhs ) @@ -695,17 +695,17 @@ let expand_as = | RProd(loc,na,t,b) -> RProd(loc,na,expand_as map t, expand_as map b) | RLetIn(loc,na,v,b) -> RLetIn(loc,na, expand_as map v,expand_as map b) | RLetTuple(loc,nal,(na,po),v,b) -> - RLetTuple(loc,nal,(na,option_map (expand_as map) po), + RLetTuple(loc,nal,(na,Option.map (expand_as map) po), expand_as map v, expand_as map b) | RIf(loc,e,(na,po),br1,br2) -> - RIf(loc,expand_as map e,(na,option_map (expand_as map) po), + RIf(loc,expand_as map e,(na,Option.map (expand_as map) po), expand_as map br1, expand_as map br2) | RRec _ -> error "Not handled RRec" | RDynamic _ -> error "Not handled RDynamic" | RCast(loc,b,CastConv(kind,t)) -> RCast(loc,expand_as map b,CastConv(kind,expand_as map t)) | RCast(loc,b,CastCoerce) -> RCast(loc,expand_as map b,CastCoerce) | RCases(loc,po,el,brl) -> - RCases(loc, option_map (expand_as map) po, List.map (fun (rt,t) -> expand_as map rt,t) el, + RCases(loc, Option.map (expand_as map) po, List.map (fun (rt,t) -> expand_as map rt,t) el, List.map (expand_as_br map) brl) and expand_as_br map (loc,idl,cpl,rt) = diff --git a/contrib/interface/blast.ml b/contrib/interface/blast.ml index 207d78b19..82fbe9c69 100644 --- a/contrib/interface/blast.ml +++ b/contrib/interface/blast.ml @@ -187,7 +187,7 @@ and e_my_find_search db_list local_db hdc concl = (e_trivial_fail_db db_list local_db) | Unfold_nth c -> unfold_in_concl [[],c] | Extern tacast -> Auto.conclPattern concl - (out_some p) tacast + (Option.get p) tacast in (free_try tac,fmt_autotactic t)) (*i @@ -400,7 +400,7 @@ and my_find_search db_list local_db hdc concl = (trivial_fail_db db_list local_db) | Unfold_nth c -> unfold_in_concl [[],c] | Extern tacast -> - conclPattern concl (out_some p) tacast)) + conclPattern concl (Option.get p) tacast)) tacl and trivial_resolve db_list local_db cl = diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml index 150b070f8..0e4f66072 100644 --- a/contrib/interface/xlate.ml +++ b/contrib/interface/xlate.ml @@ -306,7 +306,7 @@ let make_fix_struct (n,bl) = let nn = List.length names in if nn = 1 || n = None then ctv_ID_OPT_NONE else - let n = out_some n in + let n = Option.get n in if n < nn then xlate_id_opt(List.nth names n) else xlate_error "unexpected result of parsing for Fixpoint";; @@ -429,7 +429,7 @@ and (xlate_formula:Topconstr.constr_expr -> Ascent.ct_FORMULA) = function (* Pierre L: could the case [n=None && bl=[]] happen ? Normally not *) (* By the way, how could [bl = []] happen in V8 syntax ? *) if bl = [] then - let n = out_some n in + let n = Option.get n in let (bl,arf,ardef) = Ppconstr.split_fix (n+1) arf ardef in (xlate_id_opt(List.nth (names_of_local_assums bl) n),bl,arf,ardef) else (make_fix_struct (n, bl),bl,arf,ardef) in @@ -995,7 +995,7 @@ and xlate_tac = let cl_as_xlate_arg = {cl_as_clause with Tacexpr.onhyps = - option_map + Option.map (fun l -> List.map (fun ((l,id),hyp_flag) -> ((l, Tacexpr.AI ((),id)) ,hyp_flag)) l ) @@ -1312,7 +1312,7 @@ and coerce_genarg_to_TARG x = (snd (out_gen (rawwit_open_constr_gen b) x)))) | ExtraArgType s as y when Pcoq.is_tactic_genarg y -> - let n = out_some (Pcoq.tactic_genarg_level s) in + let n = Option.get (Pcoq.tactic_genarg_level s) in let t = xlate_tactic (out_gen (Pcoq.rawwit_tactic n) x) in CT_coerce_TACTIC_COM_to_TARG t | ConstrWithBindingsArgType -> xlate_error "TODO: generic constr with bindings" @@ -1405,7 +1405,7 @@ let coerce_genarg_to_VARG x = | ConstrMayEvalArgType -> xlate_error"TODO: generic constr-may-eval argument" | QuantHypArgType ->xlate_error"TODO: generic quantified hypothesis argument" | ExtraArgType s as y when Pcoq.is_tactic_genarg y -> - let n = out_some (Pcoq.tactic_genarg_level s) in + let n = Option.get (Pcoq.tactic_genarg_level s) in let t = xlate_tactic (out_gen (Pcoq.rawwit_tactic n) x) in CT_coerce_TACTIC_OPT_to_VARG (CT_coerce_TACTIC_COM_to_TACTIC_OPT t) | OpenConstrArgType _ -> xlate_error "TODO: generic open constr" @@ -1857,7 +1857,7 @@ let rec xlate_vernac = CT_theorem_goal (CT_coerce_THM_to_DEFN_OR_THM (xlate_thm k), xlate_ident s, xlate_binder_list bl, xlate_formula c)) | VernacSuspend -> CT_suspend - | VernacResume idopt -> CT_resume (xlate_ident_opt (option_map snd idopt)) + | VernacResume idopt -> CT_resume (xlate_ident_opt (Option.map snd idopt)) | VernacDefinition (k,(_,s),ProveBody (bl,typ),_) -> CT_coerce_THEOREM_GOAL_to_COMMAND (CT_theorem_goal @@ -1900,7 +1900,7 @@ let rec xlate_vernac = (_, (add_coercion, (_,s)), binders, c1, rec_constructor_or_none, field_list) -> let record_constructor = - xlate_ident_opt (option_map snd rec_constructor_or_none) in + xlate_ident_opt (Option.map snd rec_constructor_or_none) in CT_record ((if add_coercion then CT_coercion_atm else CT_coerce_NONE_to_COERCION_OPT(CT_none)), @@ -1923,7 +1923,7 @@ let rec xlate_vernac = (* Pierre L: could the case [n=None && bl=[]] happen ? Normally not *) (* By the way, how could [bl = []] happen in V8 syntax ? *) if bl = [] then - let n = out_some n in + let n = Option.get n in let (bl,arf,ardef) = Ppconstr.split_fix (n+1) arf ardef in (xlate_id_opt(List.nth (names_of_local_assums bl) n),bl,arf,ardef) else (make_fix_struct (n, bl),bl,arf,ardef) in diff --git a/contrib/ring/ring.ml b/contrib/ring/ring.ml index e81c9ddd5..97dd2f143 100644 --- a/contrib/ring/ring.ml +++ b/contrib/ring/ring.ml @@ -193,7 +193,7 @@ let _ = let subst_morph subst morph = let plusm' = subst_mps subst morph.plusm in let multm' = subst_mps subst morph.multm in - let oppm' = option_smartmap (subst_mps subst) morph.oppm in + let oppm' = Option.smartmap (subst_mps subst) morph.oppm in if plusm' == morph.plusm && multm' == morph.multm && oppm' == morph.oppm then @@ -215,15 +215,15 @@ let subst_set subst cset = if !same then cset else cset' let subst_theory subst th = - let th_equiv' = option_smartmap (subst_mps subst) th.th_equiv in - let th_setoid_th' = option_smartmap (subst_mps subst) th.th_setoid_th in - let th_morph' = option_smartmap (subst_morph subst) th.th_morph in + let th_equiv' = Option.smartmap (subst_mps subst) th.th_equiv in + let th_setoid_th' = Option.smartmap (subst_mps subst) th.th_setoid_th in + let th_morph' = Option.smartmap (subst_morph subst) th.th_morph in let th_a' = subst_mps subst th.th_a in let th_plus' = subst_mps subst th.th_plus in let th_mult' = subst_mps subst th.th_mult in let th_one' = subst_mps subst th.th_one in let th_zero' = subst_mps subst th.th_zero in - let th_opp' = option_smartmap (subst_mps subst) th.th_opp in + let th_opp' = Option.smartmap (subst_mps subst) th.th_opp in let th_eq' = subst_mps subst th.th_eq in let th_t' = subst_mps subst th.th_t in let th_closed' = subst_set subst th.th_closed in diff --git a/contrib/setoid_ring/newring.ml4 b/contrib/setoid_ring/newring.ml4 index 1cbae1e2f..2c6e0ebcd 100644 --- a/contrib/setoid_ring/newring.ml4 +++ b/contrib/setoid_ring/newring.ml4 @@ -451,7 +451,7 @@ let (theory_to_obj, obj_to_theory) = let setoid_of_relation r = lapp coq_mk_Setoid [|r.rel_a; r.rel_aeq; - out_some r.rel_refl; out_some r.rel_sym; out_some r.rel_trans |] + Option.get r.rel_refl; Option.get r.rel_sym; Option.get r.rel_trans |] let op_morph r add mul opp req m1 m2 m3 = lapp coq_mk_reqe [| r; add; mul; opp; req; m1; m2; m3 |] diff --git a/contrib/subtac/subtac_cases.ml b/contrib/subtac/subtac_cases.ml index e54c59058..34c398289 100644 --- a/contrib/subtac/subtac_cases.ml +++ b/contrib/subtac/subtac_cases.ml @@ -385,7 +385,7 @@ let mkDeclTomatch na = function let map_tomatch_type f = function | IsInd (t,ind) -> IsInd (f t,map_inductive_type f ind) - | NotInd (c,t) -> NotInd (option_map f c, f t) + | NotInd (c,t) -> NotInd (Option.map f c, f t) let liftn_tomatch_type n depth = map_tomatch_type (liftn n depth) let lift_tomatch_type n = liftn_tomatch_type n 1 @@ -1127,7 +1127,7 @@ let rec generalize_problem pb = function let tomatch = regeneralize_index_tomatch (i+1) tomatch in { pb with tomatch = Abstract d :: tomatch; - pred = option_map (generalize_predicate i d) pb'.pred } + pred = Option.map (generalize_predicate i d) pb'.pred } (* No more patterns: typing the right-hand-side of equations *) let build_leaf pb = @@ -1142,7 +1142,7 @@ let build_leaf pb = let shift_problem (current,t) pb = {pb with tomatch = Alias (current,current,NonDepAlias,type_of_tomatch t)::pb.tomatch; - pred = option_map (specialize_predicate_var (current,t)) pb.pred; + pred = Option.map (specialize_predicate_var (current,t)) pb.pred; history = push_history_pattern 0 AliasLeaf pb.history; mat = List.map remove_current_pattern pb.mat } @@ -1207,7 +1207,7 @@ let build_branch current deps pb eqns const_info = let cur_alias = lift (List.length sign) current in let currents = Alias (ci,cur_alias,alias_type,ind) :: currents in let env' = push_rels sign pb.env in - let pred' = option_map (specialize_predicate (List.rev typs') dep_sign const_info) pb.pred in + let pred' = Option.map (specialize_predicate (List.rev typs') dep_sign const_info) pb.pred in sign, { pb with env = env'; @@ -1279,7 +1279,7 @@ and compile_generalization pb d rest = { pb with env = push_rel d pb.env; tomatch = rest; - pred = option_map ungeneralize_predicate pb.pred; + pred = Option.map ungeneralize_predicate pb.pred; mat = List.map (push_rels_eqn [d]) pb.mat } in let j = compile pb in { uj_val = mkLambda_or_LetIn d j.uj_val; @@ -1304,7 +1304,7 @@ and compile_alias pb (deppat,nondeppat,d,t) rest = {pb with env = newenv; tomatch = tomatch; - pred = option_map (lift_predicate n) pb.pred; + pred = Option.map (lift_predicate n) pb.pred; history = history; mat = mat } in let j = compile pb in @@ -1487,7 +1487,7 @@ let extract_arity_signature env0 tomatchl tmsign = match tm with | NotInd (bo,typ) -> (match t with - | None -> [na,option_map (lift n) bo,lift n typ] + | None -> [na,Option.map (lift n) bo,lift n typ] | Some (loc,_,_,_) -> user_err_loc (loc,"", str "Unexpected type annotation for a term of non inductive type")) @@ -1765,14 +1765,14 @@ let subst_rel_context k ctx subst = let (_, ctx') = List.fold_right (fun (n, b, t) (k, acc) -> - (succ k, (n, option_map (substnl subst k) b, substnl subst k t) :: acc)) + (succ k, (n, Option.map (substnl subst k) b, substnl subst k t) :: acc)) ctx (k, []) in ctx' let lift_rel_contextn n k sign = let rec liftrec k = function | (na,c,t)::sign -> - (na,option_map (liftn n k) c,liftn n k t)::(liftrec (k-1) sign) + (na,Option.map (liftn n k) c,liftn n k t)::(liftrec (k-1) sign) | [] -> [] in liftrec (rel_context_length sign + k) sign @@ -2065,7 +2065,7 @@ let build_dependent_signature env evars avoid tomatchs arsign = let liftn_rel_context n k sign = let rec liftrec k = function | (na,c,t)::sign -> - (na,option_map (liftn n k) c,liftn n k t)::(liftrec (k-1) sign) + (na,Option.map (liftn n k) c,liftn n k t)::(liftrec (k-1) sign) | [] -> [] in liftrec (k + rel_context_length sign) sign @@ -2074,10 +2074,10 @@ let nf_evars_env evar_defs (env : env) : env = let nf t = nf_isevar evar_defs t in let env0 : env = reset_context env in let f e (na, b, t) e' : env = - Environ.push_named (na, option_map nf b, nf t) e' + Environ.push_named (na, Option.map nf b, nf t) e' in let env' = Environ.fold_named_context f ~init:env0 env in - Environ.fold_rel_context (fun e (na, b, t) e' -> Environ.push_rel (na, option_map nf b, nf t) e') + Environ.fold_rel_context (fun e (na, b, t) e' -> Environ.push_rel (na, Option.map nf b, nf t) e') ~init:env' env let compile_cases loc (typing_fun, isevars) (tycon : Evarutil.type_constraint) env (predopt, tomatchl, eqns) = diff --git a/contrib/subtac/subtac_coercion.ml b/contrib/subtac/subtac_coercion.ml index 1fb079fac..17bbb65bd 100644 --- a/contrib/subtac/subtac_coercion.ml +++ b/contrib/subtac/subtac_coercion.ml @@ -305,7 +305,7 @@ module Coercion = struct let coerce_itf loc env isevars v t c1 = let evars = ref isevars in let coercion = coerce loc env evars t c1 in - !evars, option_map (app_opt coercion) v, t + !evars, Option.map (app_opt coercion) v, t (* Taken from pretyping/coercion.ml *) @@ -439,7 +439,7 @@ module Coercion = struct (match kind_of_term (whd_betadeltaiota env (evars_of isevars) t), kind_of_term (whd_betadeltaiota env (evars_of isevars) c1) with | Prod (_,t1,t2), Prod (name,u1,u2) -> - let v' = option_map (whd_betadeltaiota env (evars_of isevars)) v in + let v' = Option.map (whd_betadeltaiota env (evars_of isevars)) v in let (evd',b) = match v' with Some v' -> @@ -455,7 +455,7 @@ module Coercion = struct let env1 = push_rel (x,None,v1) env in let (evd'', v2', t2') = inh_conv_coerce_to_fail loc env1 evd' (Some v2) t2 u2 in - (evd'', option_map (fun v2' -> mkLambda (x, v1, v2')) v2', + (evd'', Option.map (fun v2' -> mkLambda (x, v1, v2')) v2', mkProd (x, v1, t2')) | None -> (* Mismatch on t1 and u1 or not a lambda: we eta-expand *) @@ -472,7 +472,7 @@ module Coercion = struct let (evd'', v2', t2') = let v2 = match v with - Some v -> option_map (fun v1' -> mkApp (lift 1 v, [|v1'|])) v1' + Some v -> Option.map (fun v1' -> mkApp (lift 1 v, [|v1'|])) v1' | None -> None and evd', t2 = match v1' with @@ -483,7 +483,7 @@ module Coercion = struct in inh_conv_coerce_to_fail loc env1 evd' v2 t2 u2 in - (evd'', option_map (fun v2' -> mkLambda (name, u1, v2')) v2', + (evd'', Option.map (fun v2' -> mkLambda (name, u1, v2')) v2', mkProd (name, u1, t2'))) | _ -> raise NoCoercion)) diff --git a/contrib/subtac/subtac_command.ml b/contrib/subtac/subtac_command.ml index d7d304279..49eab5d29 100644 --- a/contrib/subtac/subtac_command.ml +++ b/contrib/subtac/subtac_command.ml @@ -159,7 +159,7 @@ let list_of_local_binders l = let lift_binders k n l = let rec aux n = function - | (id, t, c) :: tl -> (id, option_map (liftn k n) t, liftn k n c) :: aux (pred n) tl + | (id, t, c) :: tl -> (id, Option.map (liftn k n) t, liftn k n c) :: aux (pred n) tl | [] -> [] in aux n l @@ -326,7 +326,7 @@ let build_wellfounded (recname, n, bl,arityc,body) r measure notation boxed = let nf_evar_context isevars ctx = List.map (fun (n, b, t) -> - (n, option_map (Evarutil.nf_isevar isevars) b, Evarutil.nf_isevar isevars t)) ctx + (n, Option.map (Evarutil.nf_isevar isevars) b, Evarutil.nf_isevar isevars t)) ctx let build_mutrec lnameargsardef boxed = let sigma = Evd.empty and env = Global.env () in diff --git a/contrib/subtac/subtac_obligations.ml b/contrib/subtac/subtac_obligations.ml index 769aff9dc..5e7f025be 100644 --- a/contrib/subtac/subtac_obligations.ml +++ b/contrib/subtac/subtac_obligations.ml @@ -58,7 +58,7 @@ let subst_deps obls deps t = let xobl = obls.(x) in debug 3 (str "Trying to get body of obligation " ++ int x); let oblb = - try out_some xobl.obl_body + try Option.get xobl.obl_body with _ -> debug 3 (str "Couldn't get body of obligation " ++ int x); assert(false) diff --git a/contrib/subtac/subtac_pretyping_F.ml b/contrib/subtac/subtac_pretyping_F.ml index ab542feb2..0ed0632c6 100644 --- a/contrib/subtac/subtac_pretyping_F.ml +++ b/contrib/subtac/subtac_pretyping_F.ml @@ -290,7 +290,7 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct let value, typ = applist (j_val resj, [j_val hj]), subst1 hj.uj_val c2 in let typ' = nf_isevar !isevars typ in let tycon = - option_map + Option.map (fun (abs, ty) -> match abs with None -> @@ -306,7 +306,7 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct apply_rec env (n+1) { uj_val = nf_isevar !isevars value; uj_type = nf_isevar !isevars typ' } - (option_map (fun (abs, c) -> abs, nf_isevar !isevars c) tycon) rest + (Option.map (fun (abs, c) -> abs, nf_isevar !isevars c) tycon) rest | _ -> let hj = pretype empty_tycon env isevars lvar c in @@ -314,7 +314,7 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct (join_loc floc argloc) env (evars_of !isevars) resj [hj] in - let ftycon = option_map (lift_abstr_tycon_type (-1)) ftycon in + let ftycon = Option.map (lift_abstr_tycon_type (-1)) ftycon in let resj = j_nf_evar (evars_of !isevars) (apply_rec env 1 fj ftycon args) in let resj = match kind_of_term resj.uj_val with diff --git a/contrib/xml/xmlcommand.ml b/contrib/xml/xmlcommand.ml index 1aabd4348..82d7c19e5 100644 --- a/contrib/xml/xmlcommand.ml +++ b/contrib/xml/xmlcommand.ml @@ -691,11 +691,11 @@ let _ = Buffer.output_buffer ch theory_buffer ; close_out ch end ; - Util.option_iter + Option.iter (fun fn -> let coqdoc = Coq_config.bindir^"/coqdoc" in let options = " --html -s --body-only --no-index --latin1 --raw-comments" in - let dir = Util.out_some xml_library_root in + let dir = Option.get xml_library_root in let command cmd = if Sys.command cmd <> 0 then Util.anomaly ("Error executing \"" ^ cmd ^ "\"") diff --git a/ide/coqide.ml b/ide/coqide.ml index 08afda00b..cda306eb2 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -13,18 +13,18 @@ open Vernacexpr open Coq open Ideutils -let out_some s = match s with - | None -> failwith "Internal error in out_some" | Some f -> f +let Option.get s = match s with + | None -> failwith "Internal error in Option.get" | Some f -> f let cb_ = ref None -let cb () = ((out_some !cb_):GData.clipboard) +let cb () = ((Option.get !cb_):GData.clipboard) let last_cb_content = ref "" let (message_view:GText.view option ref) = ref None let (proof_view:GText.view option ref) = ref None let (_notebook:GPack.notebook option ref) = ref None -let notebook () = out_some !_notebook +let notebook () = Option.get !_notebook let update_notebook_pos () = let pos = @@ -99,7 +99,7 @@ module Vector = struct type 'a t = ('a option) array ref let create () = ref [||] let length t = Array.length !t - let get t i = out_some (Array.get !t i) + let get t i = Option.get (Array.get !t i) let set t i v = Array.set !t i (Some v) let remove t i = Array.set !t i None let append t e = t := Array.append !t [|Some e|]; (Array.length !t)-1 @@ -111,7 +111,7 @@ module Vector = struct let exists f t = let l = Array.length !t in let rec test i = - (i < l) && (((!t.(i) <> None) && f (out_some !t.(i))) || test (i+1)) + (i < l) && (((!t.(i) <> None) && f (Option.get !t.(i))) || test (i+1)) in test 0 end @@ -310,7 +310,7 @@ let get_input_view i = let active_view = ref None -let get_active_view () = Vector.get input_views (out_some !active_view) +let get_active_view () = Vector.get input_views (Option.get !active_view) let set_active_view i = (match !active_view with None -> () | Some i -> @@ -461,7 +461,7 @@ let rec complete input_buffer w (offset:int) = end let get_current_word () = - let av = out_some ((get_current_view ()).analyzed_view) in + let av = Option.get ((get_current_view ()).analyzed_view) in match GtkBase.Clipboard.wait_for_text (cb ())#as_clipboard with | None -> prerr_endline "None selected"; @@ -566,11 +566,11 @@ let activate_input i = (match !active_view with | None -> () | Some n -> - let a_v = out_some (Vector.get input_views n).analyzed_view in + let a_v = Option.get (Vector.get input_views n).analyzed_view in a_v#deactivate (); a_v#reset_initial ); - let activate_function = (out_some (Vector.get input_views i).analyzed_view)#activate in + let activate_function = (Option.get (Vector.get input_views i).analyzed_view)#activate in activate_function (); set_active_view i @@ -585,13 +585,13 @@ let warning msg = class analyzed_view index = let {view = input_view_} as current_all_ = get_input_view index in - let proof_view_ = out_some !proof_view in - let message_view_ = out_some !message_view in + let proof_view_ = Option.get !proof_view in + let message_view_ = Option.get !message_view in object(self) val current_all = current_all_ val input_view = current_all_.view - val proof_view = out_some !proof_view - val message_view = out_some !message_view + val proof_view = Option.get !proof_view + val message_view = Option.get !message_view val input_buffer = input_view_#buffer val proof_buffer = proof_view_#buffer val message_buffer = message_view_#buffer @@ -1008,7 +1008,7 @@ object(self) self#insert_message s; message_view#misc#draw None; if localize then - (match Util.option_map Util.unloc loc with + (match Option.map Util.unloc loc with | None -> () | Some (start,stop) -> let convert_pos = byte_offset_to_char_offset phrase in @@ -1541,7 +1541,7 @@ Please restart and report NOW."; deact_id <- Some (input_view#event#connect#key_press self#disconnected_keypress_handler); prerr_endline "CONNECTED inactive : "; - print_id (out_some deact_id) + print_id (Option.get deact_id) method activate () = is_active <- true; @@ -1553,9 +1553,9 @@ Please restart and report NOW."; act_id <- Some (input_view#event#connect#key_press self#active_keypress_handler); prerr_endline "CONNECTED active : "; - print_id (out_some act_id); + print_id (Option.get act_id); match - (out_some ((Vector.get input_views index).analyzed_view)) #filename + (Option.get ((Vector.get input_views index).analyzed_view)) #filename with | None -> () | Some f -> let dir = Filename.dirname f in @@ -1653,7 +1653,7 @@ Please restart and report NOW."; if auto_complete_on && String.length s = 1 && s <> " " && s <> "\n" then - let v = out_some (get_current_view ()).analyzed_view + let v = Option.get (get_current_view ()).analyzed_view in let has_completed = v#complete_at_offset @@ -1670,7 +1670,7 @@ Please restart and report NOW."; (fun () -> if input_buffer#modified then set_tab_image index - ~icon:(match (out_some (current_all.analyzed_view))#filename with + ~icon:(match (Option.get (current_all.analyzed_view))#filename with | None -> `SAVE_AS | Some _ -> `SAVE ) @@ -1924,20 +1924,20 @@ let main files = let save_f () = let current = get_current_view () in try - (match (out_some current.analyzed_view)#filename with + (match (Option.get current.analyzed_view)#filename with | None -> begin match GToolbox.select_file ~title:"Save file" () with | None -> () | Some f -> - if (out_some current.analyzed_view)#save_as f then begin + if (Option.get current.analyzed_view)#save_as f then begin set_current_tab_label (Filename.basename f); !flash_info ("File " ^ f ^ " saved") end else warning ("Save Failed (check if " ^ f ^ " is writable)") end | Some f -> - if (out_some current.analyzed_view)#save f then + if (Option.get current.analyzed_view)#save f then !flash_info ("File " ^ f ^ " saved") else warning ("Save Failed (check if " ^ f ^ " is writable)") @@ -1952,13 +1952,13 @@ let main files = in let saveas_f () = let current = get_current_view () in - try (match (out_some current.analyzed_view)#filename with + try (match (Option.get current.analyzed_view)#filename with | None -> begin match GToolbox.select_file ~title:"Save file as" () with | None -> () | Some f -> - if (out_some current.analyzed_view)#save_as f then begin + if (Option.get current.analyzed_view)#save_as f then begin set_current_tab_label (Filename.basename f); !flash_info "Saved" end @@ -1972,7 +1972,7 @@ let main files = with | None -> () | Some f -> - if (out_some current.analyzed_view)#save_as f then begin + if (Option.get current.analyzed_view)#save_as f then begin set_current_tab_label (Filename.basename f); !flash_info "Saved" end else !flash_info "Save Failed" @@ -2028,7 +2028,7 @@ let main files = let close_m = file_factory#add_item "_Close Buffer" ~key:GdkKeysyms._W in let close_f () = - let v = out_some !active_view in + let v = Option.get !active_view in let act = get_current_view_page () in if v = act then !flash_info "Cannot close an active view" else remove_current_view_page () @@ -2038,7 +2038,7 @@ let main files = (* File/Print Menu *) let print_f () = let v = get_current_view () in - let av = out_some v.analyzed_view in + let av = Option.get v.analyzed_view in match av#filename with | None -> !flash_info "Cannot print: this buffer has no name" @@ -2058,7 +2058,7 @@ let main files = (* File/Export to Menu *) let export_f kind () = let v = get_current_view () in - let av = out_some v.analyzed_view in + let av = Option.get v.analyzed_view in match av#filename with | None -> !flash_info "Cannot print: this buffer has no name" @@ -2103,7 +2103,7 @@ let main files = (fun () -> Highlight.highlight_all (get_current_view()).view#buffer; - (out_some (get_current_view()).analyzed_view)#recenter_insert)); + (Option.get (get_current_view()).analyzed_view)#recenter_insert)); (* File/Quit Menu *) let quit_f () = @@ -2137,7 +2137,7 @@ let main files = ignore(edit_f#add_item "_Undo" ~key:GdkKeysyms._u ~callback: (do_if_not_computing "undo" (fun () -> - ignore ((out_some ((get_current_view()).analyzed_view))# + ignore ((Option.get ((get_current_view()).analyzed_view))# without_auto_complete (fun () -> (get_current_view()).view#undo) ())))); ignore(edit_f#add_item "_Clear Undo Stack" @@ -2393,7 +2393,7 @@ let main files = ~callback: (do_if_not_computing (fun b -> - let v = out_some (get_current_view ()).analyzed_view + let v = Option.get (get_current_view ()).analyzed_view in v#complete_at_offset ((v#view#buffer#get_iter `SEL_BOUND)#offset) @@ -2405,7 +2405,7 @@ let main files = ignore(edit_f#add_item "Complete Word" ~key:GdkKeysyms._slash ~callback: (fun () -> ignore ( - let av = out_some ((get_current_view()).analyzed_view) in + let av = Option.get ((get_current_view()).analyzed_view) in av#complete_at_offset (av#get_insert)#offset ))); @@ -2414,7 +2414,7 @@ let main files = let _ = edit_f#add_item "External editor" ~callback: (fun () -> - let av = out_some ((get_current_view()).analyzed_view) in + let av = Option.get ((get_current_view()).analyzed_view) in match av#filename with | None -> () | Some f -> @@ -2480,7 +2480,7 @@ let main files = in let do_or_activate f () = let current = get_current_view () in - let analyzed_view = out_some current.analyzed_view in + let analyzed_view = Option.get current.analyzed_view in if analyzed_view#is_active then ignore (f analyzed_view) else @@ -2565,7 +2565,7 @@ let main files = in let do_if_active_raw f () = let current = get_current_view () in - let analyzed_view = out_some current.analyzed_view in + let analyzed_view = Option.get current.analyzed_view in if analyzed_view#is_active then ignore (f analyzed_view) in let do_if_active f = @@ -2858,7 +2858,7 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S); (* Command/Compile Menu *) let compile_f () = let v = get_current_view () in - let av = out_some v.analyzed_view in + let av = Option.get v.analyzed_view in save_f (); match av#filename with | None -> @@ -2885,7 +2885,7 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S); (* Command/Make Menu *) let make_f () = let v = get_current_view () in - let av = out_some v.analyzed_view in + let av = Option.get v.analyzed_view in match av#filename with | None -> !flash_info "Cannot make: this buffer has no name" @@ -2914,7 +2914,7 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S); let file,line,start,stop,error_msg = search_next_error () in load file; let v = get_current_view () in - let av = out_some v.analyzed_view in + let av = Option.get v.analyzed_view in let input_buffer = v.view#buffer in (* let init = input_buffer#start_iter in @@ -2940,7 +2940,7 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S); with Not_found -> last_make_index := 0; let v = get_current_view () in - let av = out_some v.analyzed_view in + let av = Option.get v.analyzed_view in av#set_message "No more errors.\n" in let _ = @@ -2952,7 +2952,7 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S); (* Command/CoqMakefile Menu*) let coq_makefile_f () = let v = get_current_view () in - let av = out_some v.analyzed_view in + let av = Option.get v.analyzed_view in match av#filename with | None -> !flash_info "Cannot make makefile: this buffer has no name" @@ -2993,7 +2993,7 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S); if nb#misc#toplevel#get_oid=w#coerce#get_oid then begin let nw = GWindow.window ~show:true () in - let parent = out_some nb#misc#parent in + let parent = Option.get nb#misc#parent in ignore (nw#connect#destroy ~callback: (fun () -> nb#misc#reparent parent)); @@ -3046,17 +3046,17 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S); let _ = help_factory#add_item "Browse Coq _Manual" ~callback: (fun () -> - let av = out_some ((get_current_view ()).analyzed_view) in + let av = Option.get ((get_current_view ()).analyzed_view) in browse av#insert_message (!current.doc_url ^ "main.html")) in let _ = help_factory#add_item "Browse Coq _Library" ~callback: (fun () -> - let av = out_some ((get_current_view ()).analyzed_view) in + let av = Option.get ((get_current_view ()).analyzed_view) in browse av#insert_message !current.library_url) in let _ = help_factory#add_item "Help for _keyword" ~key:GdkKeysyms._F1 ~callback:(fun () -> - let av = out_some ((get_current_view ()).analyzed_view) in + let av = Option.get ((get_current_view ()).analyzed_view) in av#help_for_keyword ()) in let _ = help_factory#add_separator () in @@ -3405,7 +3405,7 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S); (fun _ -> if !current.contextual_menus_on_goal then begin - let w = (out_some (get_active_view ()).analyzed_view) in + let w = (Option.get (get_active_view ()).analyzed_view) in !push_info "Computing advanced goal's menus"; prerr_endline "Entering Goal Window. Computing Menus...."; w#show_goals_full; diff --git a/interp/constrextern.ml b/interp/constrextern.ml index ec88e6fe8..ec74c91b2 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -233,11 +233,6 @@ and check_same_fix_binder bl1 bl2 = let same c d = try check_same_type c d; true with _ -> false (* Idem for rawconstr *) -let option_iter2 f o1 o2 = - match o1, o2 with - Some o1, Some o2 -> f o1 o2 - | None, None -> () - | _ -> failwith "option" let array_iter2 f v1 v2 = List.iter2 f (Array.to_list v1) (Array.to_list v2) @@ -256,7 +251,7 @@ let rec same_raw c d = | RVar(_,id1), RVar(_,id2) -> if id1<>id2 then failwith "RVar" | REvar(_,e1,a1), REvar(_,e2,a2) -> if e1 <> e2 then failwith "REvar"; - option_iter2(List.iter2 same_raw) a1 a2 + Option.iter2(List.iter2 same_raw) a1 a2 | RPatVar(_,pv1), RPatVar(_,pv2) -> if pv1<>pv2 then failwith "RPatVar" | RApp(_,f1,a1), RApp(_,f2,a2) -> List.iter2 same_raw (f1::a1) (f2::a2) @@ -274,7 +269,7 @@ let rec same_raw c d = (fun (t1,(al1,oind1)) (t2,(al2,oind2)) -> same_raw t1 t2; if al1 <> al2 then failwith "RCases"; - option_iter2(fun (_,i1,_,nl1) (_,i2,_,nl2) -> + Option.iter2(fun (_,i1,_,nl1) (_,i2,_,nl2) -> if i1<>i2 || nl1 <> nl2 then failwith "RCases") oind1 oind2) c1 c2; List.iter2 (fun (_,_,pl1,b1) (_,_,pl2,b2) -> List.iter2 same_patt pl1 pl2; @@ -290,7 +285,7 @@ let rec same_raw c d = array_iter2 (List.iter2 (fun (na1,bd1,ty1) (na2,bd2,ty2) -> if na1<>na2 then failwith "RRec"; - option_iter2 same_raw bd1 bd2; + Option.iter2 same_raw bd1 bd2; same_raw ty1 ty2)) bl1 bl2; array_iter2 same_raw ty1 ty2; array_iter2 same_raw def1 def2 @@ -659,7 +654,7 @@ let rec extern inctx scopes vars r = | REvar (loc,n,None) when !print_meta_as_hole -> CHole loc | REvar (loc,n,l) -> - extern_evar loc n (option_map (List.map (extern false scopes vars)) l) + extern_evar loc n (Option.map (List.map (extern false scopes vars)) l) | RPatVar (loc,n) -> if !print_meta_as_hole then CHole loc else CPatVar (loc,n) @@ -699,17 +694,17 @@ let rec extern inctx scopes vars r = let vars' = List.fold_right (name_fold Idset.add) (cases_predicate_names tml) vars in - let rtntypopt' = option_map (extern_typ scopes vars') rtntypopt in + let rtntypopt' = Option.map (extern_typ scopes vars') rtntypopt in let tml = List.map (fun (tm,(na,x)) -> let na' = match na,tm with Anonymous, RVar (_,id) when - rtntypopt<>None & occur_rawconstr id (out_some rtntypopt) + rtntypopt<>None & occur_rawconstr id (Option.get rtntypopt) -> Some Anonymous | Anonymous, _ -> None | Name id, RVar (_,id') when id=id' -> None | Name _, _ -> Some na in (sub_extern false scopes vars tm, - (na',option_map (fun (loc,ind,n,nal) -> + (na',Option.map (fun (loc,ind,n,nal) -> let params = list_tabulate (fun _ -> RHole (dummy_loc,Evd.InternalHole)) n in let args = List.map (function @@ -722,15 +717,15 @@ let rec extern inctx scopes vars r = | RLetTuple (loc,nal,(na,typopt),tm,b) -> CLetTuple (loc,nal, - (option_map (fun _ -> na) typopt, - option_map (extern_typ scopes (add_vname vars na)) typopt), + (Option.map (fun _ -> na) typopt, + Option.map (extern_typ scopes (add_vname vars na)) typopt), sub_extern false scopes vars tm, extern false scopes (List.fold_left add_vname vars nal) b) | RIf (loc,c,(na,typopt),b1,b2) -> CIf (loc,sub_extern false scopes vars c, - (option_map (fun _ -> na) typopt, - option_map (extern_typ scopes (add_vname vars na)) typopt), + (Option.map (fun _ -> na) typopt, + Option.map (extern_typ scopes (add_vname vars na)) typopt), sub_extern false scopes vars b1, sub_extern false scopes vars b2) | RRec (loc,fk,idv,blv,tyv,bv) -> @@ -949,12 +944,12 @@ let rec raw_of_pat env = function let brs = Array.to_list (Array.map (raw_of_pat env) bv) in let brns = Array.to_list cstr_nargs in (* ind is None only if no branch and no return type *) - let ind = out_some indo in + let ind = Option.get indo in let mat = simple_cases_matrix_of_branches ind brns brs in let indnames,rtn = if p = PMeta None then (Anonymous,None),None else - let nparams,n = out_some ind_nargs in + let nparams,n = Option.get ind_nargs in return_type_of_predicate ind nparams n (raw_of_pat env p) in RCases (loc,rtn,[raw_of_pat env tm,indnames],mat) | PFix f -> Detyping.detype false [] env (mkFix f) diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 0d9f95795..6fc7a7d31 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -226,7 +226,7 @@ let make_current_scope (tmp_scope,scopes) = option_cons tmp_scope scopes let set_var_scope loc id (_,scopt,scopes) varscopes = let idscopes = List.assoc id varscopes in if !idscopes <> None & - make_current_scope (out_some !idscopes) + make_current_scope (Option.get !idscopes) <> make_current_scope (scopt,scopes) then user_err_loc (loc,"set_var_scope", pr_id id ++ str " already occurs in a different scope") @@ -796,7 +796,7 @@ let internalise sigma globalenv env allow_patvar lvar c = let idl = Array.map (fun (id,(n,order),bl,ty,bd) -> let intern_ro_arg c f = - let before, after = list_chop (succ (out_some n)) bl in + let before, after = list_chop (succ (Option.get n)) bl in let ((ids',_,_),rafter) = List.fold_left intern_local_binder (env,[]) after in let ro = (intern (ids', tmp_scope, scopes) c) in @@ -898,21 +898,21 @@ let internalise sigma globalenv env allow_patvar lvar c = let (tm,ind),nal = intern_case_item env citm in (tm,ind)::inds,List.fold_left (push_name_env lvar) env nal) tms ([],env) in - let rtnpo = option_map (intern_type env') rtnpo in + let rtnpo = Option.map (intern_type env') rtnpo in let eqns' = List.map (intern_eqn (List.length tms) env) eqns in RCases (loc, rtnpo, tms, List.flatten eqns') | CLetTuple (loc, nal, (na,po), b, c) -> let env' = reset_tmp_scope env in let ((b',(na',_)),ids) = intern_case_item env' (b,(na,None)) in let env'' = List.fold_left (push_name_env lvar) env ids in - let p' = option_map (intern_type env'') po in + let p' = Option.map (intern_type env'') po in RLetTuple (loc, nal, (na', p'), b', intern (List.fold_left (push_name_env lvar) env nal) c) | CIf (loc, c, (na,po), b1, b2) -> let env' = reset_tmp_scope env in let ((c',(na',_)),ids) = intern_case_item env' (c,(na,None)) in let env'' = List.fold_left (push_name_env lvar) env ids in - let p' = option_map (intern_type env'') po in + let p' = Option.map (intern_type env'') po in RIf (loc, c', (na', p'), intern env b1, intern env b2) | CHole loc -> RHole (loc, Evd.QuestionMark true) @@ -921,7 +921,7 @@ let internalise sigma globalenv env allow_patvar lvar c = | CPatVar (loc, _) -> raise (InternalisationError (loc,NegativeMetavariable)) | CEvar (loc, n, l) -> - REvar (loc, n, option_map (List.map (intern env)) l) + REvar (loc, n, Option.map (List.map (intern env)) l) | CSort (loc, s) -> RSort(loc,s) | CCast (loc, c1, CastConv (k, c2)) -> diff --git a/interp/genarg.ml b/interp/genarg.ml index 930cfe739..fc93f455a 100644 --- a/interp/genarg.ml +++ b/interp/genarg.ml @@ -223,7 +223,7 @@ let app_list1 f = function let app_opt f = function | (OptArgType t as u, l) -> let o = Obj.magic l in - (u, Obj.repr (option_map (fun x -> out_gen t (f (in_gen t x))) o)) + (u, Obj.repr (Option.map (fun x -> out_gen t (f (in_gen t x))) o)) | _ -> failwith "Genarg: not an opt" let app_pair f1 f2 = function diff --git a/interp/notation.ml b/interp/notation.ml index aaab6a933..d5de23bc5 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -133,7 +133,7 @@ let push_scopes = List.fold_right push_scope type local_scopes = tmp_scope_name option * scope_name list let make_current_scopes (tmp_scope,scopes) = - option_fold_right push_scope tmp_scope (push_scopes scopes !scope_stack) + Option.fold_right push_scope tmp_scope (push_scopes scopes !scope_stack) (**********************************************************************) (* Delimiters *) @@ -143,7 +143,7 @@ let delimiters_map = ref Gmap.empty let declare_delimiters scope key = let sc = find_scope scope in if sc.delimiters <> None && Options.is_verbose () then begin - let old = out_some sc.delimiters in + let old = Option.get sc.delimiters in Options.if_verbose warning ("Overwritting previous delimiting key "^old^" in scope "^scope) end; @@ -239,12 +239,12 @@ let delay dir int loc x = (dir, (fun () -> int loc x)) let declare_numeral_interpreter sc dir interp (patl,uninterp,inpat) = declare_prim_token_interpreter sc (fun cont loc -> function Numeral n-> delay dir interp loc n | p -> cont loc p) - (patl, (fun r -> option_map mkNumeral (uninterp r)), inpat) + (patl, (fun r -> Option.map mkNumeral (uninterp r)), inpat) let declare_string_interpreter sc dir interp (patl,uninterp,inpat) = declare_prim_token_interpreter sc (fun cont loc -> function String s -> delay dir interp loc s | p -> cont loc p) - (patl, (fun r -> option_map mkString (uninterp r)), inpat) + (patl, (fun r -> Option.map mkString (uninterp r)), inpat) let check_required_module loc sc (sp,d) = try let _ = Nametab.absolute_reference sp in () @@ -396,7 +396,7 @@ let uninterp_prim_token_cases_pattern c = let availability_of_prim_token printer_scope local_scopes = let f scope = Hashtbl.mem prim_token_interpreter_tab scope in let scopes = make_current_scopes local_scopes in - option_map snd (find_without_delimiters f (Some printer_scope,None) scopes) + Option.map snd (find_without_delimiters f (Some printer_scope,None) scopes) (* Miscellaneous *) @@ -454,7 +454,7 @@ type arguments_scope_discharge_request = | ArgsScopeNoDischarge let load_arguments_scope _ (_,(_,r,scl)) = - List.iter (option_iter check_scope) scl; + List.iter (Option.iter check_scope) scl; arguments_scope := Refmap.add r scl !arguments_scope let cache_arguments_scope o = diff --git a/interp/reserve.ml b/interp/reserve.ml index 5a8eafff7..131ce2970 100644 --- a/interp/reserve.ml +++ b/interp/reserve.ml @@ -59,17 +59,17 @@ let rec unloc = function | RLetIn (_,na,b,c) -> RLetIn (dummy_loc,na,unloc b,unloc c) | RCases (_,rtntypopt,tml,pl) -> RCases (dummy_loc, - (option_map unloc rtntypopt), + (Option.map unloc rtntypopt), List.map (fun (tm,x) -> (unloc tm,x)) tml, List.map (fun (_,idl,p,c) -> (dummy_loc,idl,p,unloc c)) pl) | RLetTuple (_,nal,(na,po),b,c) -> - RLetTuple (dummy_loc,nal,(na,option_map unloc po),unloc b,unloc c) + RLetTuple (dummy_loc,nal,(na,Option.map unloc po),unloc b,unloc c) | RIf (_,c,(na,po),b1,b2) -> - RIf (dummy_loc,unloc c,(na,option_map unloc po),unloc b1,unloc b2) + RIf (dummy_loc,unloc c,(na,Option.map unloc po),unloc b1,unloc b2) | RRec (_,fk,idl,bl,tyl,bv) -> RRec (dummy_loc,fk,idl, Array.map (List.map - (fun (na,obd,ty) -> (na,option_map unloc obd, unloc ty))) + (fun (na,obd,ty) -> (na,Option.map unloc obd, unloc ty))) bl, Array.map unloc tyl, Array.map unloc bv) diff --git a/interp/topconstr.ml b/interp/topconstr.ml index a44f0b6b4..fcf383937 100644 --- a/interp/topconstr.ml +++ b/interp/topconstr.ml @@ -94,14 +94,14 @@ let rawconstr_of_aconstr_with_binders loc g f e = function let ((idl,e),patl) = list_fold_map (cases_pattern_fold_map loc fold) ([],e) patl in (loc,idl,patl,f e rhs)) eqnl in - RCases (loc,option_map (f e') rtntypopt,tml',eqnl') + RCases (loc,Option.map (f e') rtntypopt,tml',eqnl') | ALetTuple (nal,(na,po),b,c) -> let e,nal = list_fold_map (name_fold_map g) e nal in let e,na = name_fold_map g e na in - RLetTuple (loc,nal,(na,option_map (f e) po),f e b,f e c) + RLetTuple (loc,nal,(na,Option.map (f e) po),f e b,f e c) | AIf (c,(na,po),b1,b2) -> let e,na = name_fold_map g e na in - RIf (loc,f e c,(na,option_map (f e) po),f e b1,f e b2) + RIf (loc,f e c,(na,Option.map (f e) po),f e b1,f e b2) | ACast (c,k) -> RCast (loc,f e c, match k with | CastConv (k,t) -> CastConv (k,f e t) @@ -185,20 +185,20 @@ let aconstr_and_vars_of_rawconstr a = | RLetIn (_,na,b,c) -> add_name found na; ALetIn (na,aux b,aux c) | RCases (_,rtntypopt,tml,eqnl) -> let f (_,idl,pat,rhs) = found := idl@(!found); (pat,aux rhs) in - ACases (option_map aux rtntypopt, + ACases (Option.map aux rtntypopt, List.map (fun (tm,(na,x)) -> add_name found na; - option_iter + Option.iter (fun (_,_,_,nl) -> List.iter (add_name found) nl) x; - (aux tm,(na,option_map (fun (_,ind,n,nal) -> (ind,n,nal)) x))) tml, + (aux tm,(na,Option.map (fun (_,ind,n,nal) -> (ind,n,nal)) x))) tml, List.map f eqnl) | RLetTuple (loc,nal,(na,po),b,c) -> add_name found na; List.iter (add_name found) nal; - ALetTuple (nal,(na,option_map aux po),aux b,aux c) + ALetTuple (nal,(na,Option.map aux po),aux b,aux c) | RIf (loc,c,(na,po),b1,b2) -> add_name found na; - AIf (aux c,(na,option_map aux po),aux b1,aux b2) + AIf (aux c,(na,Option.map aux po),aux b1,aux b2) | RCast (_,c,k) -> ACast (aux c, match k with CastConv (k,t) -> CastConv (k,aux t) | CastCoerce -> CastCoerce) @@ -305,11 +305,11 @@ let rec subst_aconstr subst bound raw = ALetIn (n,r1',r2') | ACases (rtntypopt,rl,branches) -> - let rtntypopt' = option_smartmap (subst_aconstr subst bound) rtntypopt + let rtntypopt' = Option.smartmap (subst_aconstr subst bound) rtntypopt and rl' = list_smartmap (fun (a,(n,signopt) as x) -> let a' = subst_aconstr subst bound a in - let signopt' = option_map (fun ((indkn,i),n,nal as z) -> + let signopt' = Option.map (fun ((indkn,i),n,nal as z) -> let indkn' = subst_kn subst indkn in if indkn == indkn' then z else ((indkn',i),n,nal)) signopt in if a' == a && signopt' == signopt then x else (a',(n,signopt'))) @@ -327,14 +327,14 @@ let rec subst_aconstr subst bound raw = ACases (rtntypopt',rl',branches') | ALetTuple (nal,(na,po),b,c) -> - let po' = option_smartmap (subst_aconstr subst bound) po + let po' = Option.smartmap (subst_aconstr subst bound) po and b' = subst_aconstr subst bound b and c' = subst_aconstr subst bound c in if po' == po && b' == b && c' == c then raw else ALetTuple (nal,(na,po'),b',c') | AIf (c,(na,po),b1,b2) -> - let po' = option_smartmap (subst_aconstr subst bound) po + let po' = Option.smartmap (subst_aconstr subst bound) po and b1' = subst_aconstr subst bound b1 and b2' = subst_aconstr subst bound b2 and c' = subst_aconstr subst bound c in @@ -368,7 +368,7 @@ let encode_list_value l = RApp (dummy_loc,RVar (dummy_loc,ldots_var),l) (* Pattern-matching rawconstr and aconstr *) let abstract_return_type_context pi mklam tml rtno = - option_map (fun rtn -> + Option.map (fun rtn -> let nal = List.flatten (List.map (fun (_,(na,t)) -> match t with Some x -> (pi x)@[na] | None -> [na]) tml) in @@ -663,8 +663,8 @@ let ids_of_cases_indtype = let ids_of_cases_tomatch tms = List.fold_right (fun (_,(ona,indnal)) l -> - option_fold_right (fun t -> (@) (ids_of_cases_indtype t)) - indnal (option_fold_right name_cons ona l)) + Option.fold_right (fun t -> (@) (ids_of_cases_indtype t)) + indnal (Option.fold_right name_cons ona l)) tms [] let is_constructor id = @@ -715,17 +715,17 @@ let fold_constr_expr_with_binders g f n acc = function acc | CCases (loc,rtnpo,al,bl) -> let ids = ids_of_cases_tomatch al in - let acc = option_fold_left (f (List.fold_right g ids n)) acc rtnpo in + let acc = Option.fold_left (f (List.fold_right g ids n)) acc rtnpo in let acc = List.fold_left (f n) acc (List.map fst al) in List.fold_right (fun (loc,patl,rhs) acc -> let ids = ids_of_pattern_list patl in f (Idset.fold g ids n) acc rhs) bl acc | CLetTuple (loc,nal,(ona,po),b,c) -> let n' = List.fold_right (name_fold g) nal n in - f (option_fold_right (name_fold g) ona n') (f n acc b) c + f (Option.fold_right (name_fold g) ona n') (f n acc b) c | CIf (_,c,(ona,po),b1,b2) -> let acc = f n (f n (f n acc b1) b2) c in - option_fold_left (f (option_fold_right (name_fold g) ona n)) acc po + Option.fold_left (f (Option.fold_right (name_fold g) ona n)) acc po | CFix (loc,_,l) -> let n' = List.fold_right (fun (id,_,_,_,_) -> g id) l n in List.fold_right (fun (_,(_,o),lb,t,c) acc -> @@ -828,15 +828,15 @@ let map_constr_expr_with_binders g f e = function (* TODO: apply g on the binding variables in pat... *) let bl = List.map (fun (loc,pat,rhs) -> (loc,pat,f e rhs)) bl in let ids = ids_of_cases_tomatch a in - let po = option_map (f (List.fold_right g ids e)) rtnpo in + let po = Option.map (f (List.fold_right g ids e)) rtnpo in CCases (loc, po, List.map (fun (tm,x) -> (f e tm,x)) a,bl) | CLetTuple (loc,nal,(ona,po),b,c) -> let e' = List.fold_right (name_fold g) nal e in - let e'' = option_fold_right (name_fold g) ona e in - CLetTuple (loc,nal,(ona,option_map (f e'') po),f e b,f e' c) + let e'' = Option.fold_right (name_fold g) ona e in + CLetTuple (loc,nal,(ona,Option.map (f e'') po),f e b,f e' c) | CIf (loc,c,(ona,po),b1,b2) -> - let e' = option_fold_right (name_fold g) ona e in - CIf (loc,f e c,(ona,option_map (f e') po),f e b1,f e b2) + let e' = Option.fold_right (name_fold g) ona e in + CIf (loc,f e c,(ona,Option.map (f e') po),f e b1,f e b2) | CFix (loc,id,dl) -> CFix (loc,id,List.map (fun (id,n,bl,t,d) -> let (e',bl') = map_local_binders f g e bl in diff --git a/kernel/cooking.ml b/kernel/cooking.ml index e9200cd75..cc5beb974 100644 --- a/kernel/cooking.ml +++ b/kernel/cooking.ml @@ -113,7 +113,7 @@ type recipe = { d_modlist : work_list } let on_body f = - option_map (fun c -> Declarations.from_val (f (Declarations.force c))) + Option.map (fun c -> Declarations.from_val (f (Declarations.force c))) let cook_constant env r = let cb = r.d_from in diff --git a/kernel/declarations.ml b/kernel/declarations.ml index eb49ba620..4a5893de8 100644 --- a/kernel/declarations.ml +++ b/kernel/declarations.ml @@ -56,7 +56,7 @@ type constant_body = { information). *) let subst_rel_declaration sub (id,copt,t as x) = - let copt' = option_smartmap (subst_mps sub) copt in + let copt' = Option.smartmap (subst_mps sub) copt in let t' = subst_mps sub t in if copt == copt' & t == t' then x else (id,copt',t') @@ -198,7 +198,7 @@ let subst_arity sub = function (* TODO: should be changed to non-coping after Term.subst_mps *) let subst_const_body sub cb = { const_hyps = (assert (cb.const_hyps=[]); []); - const_body = option_map (subst_constr_subst sub) cb.const_body; + const_body = Option.map (subst_constr_subst sub) cb.const_body; const_type = subst_arity sub cb.const_type; const_body_code = Cemitcodes.subst_to_patch_subst sub cb.const_body_code; (*const_type_code = Cemitcodes.subst_to_patch sub cb.const_type_code;*) @@ -241,7 +241,7 @@ let subst_mind sub mib = map_rel_context (subst_mps sub) mib.mind_params_ctxt; mind_packets = array_smartmap (subst_mind_packet sub) mib.mind_packets ; mind_constraints = mib.mind_constraints ; - mind_equiv = option_map (subst_kn sub) mib.mind_equiv } + mind_equiv = Option.map (subst_kn sub) mib.mind_equiv } (*s Modules: signature component specifications, module types, and diff --git a/kernel/environ.ml b/kernel/environ.ml index faf075712..c2ec6ea7e 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -89,7 +89,7 @@ let named_context_of_val = fst *** /!\ *** [f t] should be convertible with t *) let map_named_val f (ctxt,ctxtv) = let ctxt = - List.map (fun (id,body,typ) -> (id, option_map f body, f typ)) ctxt in + List.map (fun (id,body,typ) -> (id, Option.map f body, f typ)) ctxt in (ctxt,ctxtv) let empty_named_context = empty_named_context diff --git a/kernel/modops.ml b/kernel/modops.ml index 8770afe13..135a37747 100644 --- a/kernel/modops.ml +++ b/kernel/modops.ml @@ -163,7 +163,7 @@ and subst_module sub mb = a module M in a signature that is knows to be equivalent to a module M' (because the signature is "K with Module M := M'") and we are substituting M' with some M''. *) - let mpo' = option_smartmap (subst_mp sub) mb.msb_equiv in + let mpo' = Option.smartmap (subst_mp sub) mb.msb_equiv in if mtb'==mb.msb_modtype && mpo'==mb.msb_equiv then mb else { msb_modtype=mtb'; msb_equiv=mpo'; @@ -274,7 +274,7 @@ let resolver_of_environment mbid modtype mp env = if expecteddef.Declarations.const_inline then let constant = lookup_constant con' env in if (not constant.Declarations.const_opaque) then - let constr = option_map Declarations.force + let constr = Option.map Declarations.force constant.Declarations.const_body in (con,constr)::(make_resolve r) else make_resolve r diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index 91e4c73fc..f7f6a980d 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -329,7 +329,7 @@ let start_module l senv = let end_module l restype senv = let oldsenv = senv.old in let modinfo = senv.modinfo in - let restype = option_map (translate_modtype senv.env) restype in + let restype = Option.map (translate_modtype senv.env) restype in let params = match modinfo.variant with | NONE | LIBRARY _ | SIG _ -> error_no_module_to_end () @@ -633,9 +633,9 @@ let import (dp,mb,depends,engmt) digest senv = let rec lighten_module mb = { mb with - mod_expr = option_map lighten_modexpr mb.mod_expr; + mod_expr = Option.map lighten_modexpr mb.mod_expr; mod_type = lighten_modtype mb.mod_type; - mod_user_type = option_map lighten_modtype mb.mod_user_type } + mod_user_type = Option.map lighten_modtype mb.mod_user_type } and lighten_modtype = function | MTBident kn as x -> x 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 diff --git a/kernel/term.ml b/kernel/term.ml index 4b01ac1cf..b09bd4aea 100644 --- a/kernel/term.ml +++ b/kernel/term.ml @@ -639,10 +639,10 @@ type strategy = types option type named_declaration = identifier * constr option * types type rel_declaration = name * constr option * types -let map_named_declaration f (id, v, ty) = (id, option_map f v, f ty) +let map_named_declaration f (id, v, ty) = (id, Option.map f v, f ty) let map_rel_declaration = map_named_declaration -let fold_named_declaration f (_, v, ty) a = f ty (option_fold_right f v a) +let fold_named_declaration f (_, v, ty) a = f ty (Option.fold_right f v a) let fold_rel_declaration = fold_named_declaration (****************************************************************************) @@ -773,7 +773,7 @@ let substl laml = substnl laml 0 let subst1 lam = substl [lam] let substnl_decl laml k (id,bodyopt,typ) = - (id,option_map (substnl laml k) bodyopt,substnl laml k typ) + (id,Option.map (substnl laml k) bodyopt,substnl laml k typ) let substl_decl laml = substnl_decl laml 0 let subst1_decl lam = substl_decl [lam] let subst1_named_decl = subst1_decl diff --git a/kernel/univ.ml b/kernel/univ.ml index fd916e77b..7a7e0bb5a 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -470,7 +470,7 @@ let is_direct_sort_constraint s v = match s with let solve_constraints_system levels level_bounds = let levels = - Array.map (option_map (function Atom u -> u | _ -> anomaly "expects Atom")) + Array.map (Option.map (function Atom u -> u | _ -> anomaly "expects Atom")) levels in let v = Array.copy level_bounds in let nind = Array.length v in diff --git a/lib/option.ml b/lib/option.ml new file mode 100644 index 000000000..96b9c70e8 --- /dev/null +++ b/lib/option.ml @@ -0,0 +1,111 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* $Id$ *) + +(** Module implementing basic combinators for OCaml option type. + It tries follow closely the style of OCaml standard library. + + Actually, some operations have the same name as [List] ones: + they actually are similar considering ['a option] as a type + of lists with at most one element. *) + +(** [has_some x] is [true] if [x] is of the form [Some y] and [false] + otherwise. *) +let has_some = function + | None -> false + | _ -> true + +exception IsNone + +(** [get x] returns [y] where [x] is [Some y]. It raises IsNone + if [x] equals [None]. *) +let get = function + | Some y -> y + | _ -> raise IsNone + + +(** [flatten x] is [Some y] if [x] is [Some (Some y)] and [None] otherwise. *) +let flatten = function + | Some (Some y) -> Some y + | _ -> None + + +(** {6 "Iterators"} ***) + +(** [iter f x] executes [f y] if [x] equals [Some y]. It does nothing + otherwise. *) +let iter f = function + | Some y -> f y + | _ -> () + + +exception Heterogeneous + +(** [iter2 f x y] executes [f z w] if [x] equals [Some z] and [y] equals + [Some w]. It does nothing if both [x] and [y] are [None]. And raises + [Heterogeneous] otherwise. *) +let iter2 f x y = + match x,y with + | Some z, Some w -> f z w + | None,None -> () + | _,_ -> raise Heterogeneous + +(** [map f x] is [None] if [x] is [None] and [Some (f y)] if [x] is [Some y]. *) +let map f = function + | Some y -> Some (f y) + | _ -> None + +(** [smartmap f x] does the same as [map f x] except that it tries to share + some memory. *) +let smartmap f = function + | Some y as x -> let y' = f y in if y' == y then x else Some y' + | _ -> None + +(** [fold_left f a x] is [f a y] if [x] is [Some y], and [a] otherwise. *) +let fold_left f a = function + | Some y -> f a y + | _ -> a + +(** [fold_right f x a] is [f y a] if [x] is [Some y], and [a] otherwise. *) +let fold_right f x a = + match x with + | Some y -> f y a + | _ -> a + + +(** {6 More Specific operations} ***) + +(** [default f x a] is [f y] if [x] is [Some y] and [a] otherwise. *) +let default f x a = + match x with + | Some y -> f y + | _ -> a + +(** [lift f x] is the same as [map f x]. *) +let lift = map + +(** [lift_right f a x] is [Some (f a y)] if [x] is [Some y], and + [None] otherwise. *) +let lift_right f a = function + | Some y -> Some (f a y) + | _ -> None + +(** [lift_left f x a] is [Some (f y a)] if [x] is [Some y], and + [None] otherwise. *) +let lift_left f x a = + match x with + | Some y -> Some (f y a) + | _ -> None + +(** [lift2 f x y] is [Some (f z w)] if [x] equals [Some z] and [y] equals + [Some w]. It is [None] otherwise. *) +let lift2 f x y = + match x,y with + | Some z, Some w -> Some (f z w) + | _,_ -> None diff --git a/lib/option.mli b/lib/option.mli new file mode 100644 index 000000000..0a22697e7 --- /dev/null +++ b/lib/option.mli @@ -0,0 +1,78 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* $Id$ *) + +(** Module implementing basic combinators for OCaml option type. + It tries follow closely the style of OCaml standard library. + + Actually, some operations have the same name as [List] ones: + they actually are similar considering ['a option] as a type + of lists with at most one element. *) + +(** [has_some x] is [true] if [x] is of the form [Some y] and [false] + otherwise. *) +val has_some : 'a option -> bool + +exception IsNone + +(** [get x] returns [y] where [x] is [Some y]. It raises IsNone + if [x] equals [None]. *) +val get : 'a option -> 'a + + +(** [flatten x] is [Some y] if [x] is [Some (Some y)] and [None] otherwise. *) +val flatten : 'a option option -> 'a option + + +(** {6 "Iterators"} ***) + +(** [iter f x] executes [f y] if [x] equals [Some y]. It does nothing + otherwise. *) +val iter : ('a -> unit) -> 'a option -> unit + +exception Heterogeneous + +(** [iter2 f x y] executes [f z w] if [x] equals [Some z] and [y] equals + [Some w]. It does nothing if both [x] and [y] are [None]. And raises + [Heterogeneous] otherwise. *) +val iter2 : ('a -> 'b -> unit) -> 'a option -> 'b option -> unit + +(** [map f x] is [None] if [x] is [None] and [Some (f y)] if [x] is [Some y]. *) +val map : ('a -> 'b) -> 'a option -> 'b option + +(** [smartmap f x] does the same as [map f x] except that it tries to share + some memory. *) +val smartmap : ('a -> 'a) -> 'a option -> 'a option + +(** [fold_left f a x] is [f a y] if [x] is [Some y], and [a] otherwise. *) +val fold_left : ('b -> 'a -> 'b) -> 'b -> 'a option -> 'b + +(** [fold_right f x a] is [f y a] if [x] is [Some y], and [a] otherwise. *) +val fold_right : ('a -> 'b -> 'b) -> 'a option -> 'b -> 'b + + +(** {6 More Specific operations} ***) + +(** [default f x a] is [f y] if [x] is [Some y] and [a] otherwise. *) +val default : ('a -> 'b) -> 'a option -> 'b -> 'b + +(** [lift f x] is the same as [map f x]. *) +val lift : ('a -> 'b) -> 'a option -> 'b option + +(** [lift_right f a x] is [Some (f a y)] if [x] is [Some y], and + [None] otherwise. *) +val lift_right : ('a -> 'b -> 'c) -> 'a -> 'b option -> 'c option + +(** [lift_left f x a] is [Some (f y a)] if [x] is [Some y], and + [None] otherwise. *) +val lift_left : ('a -> 'b -> 'c) -> 'a option -> 'b -> 'c option + +(** [lift2 f x y] is [Some (f z w)] if [x] equals [Some z] and [y] equals + [Some w]. It is [None] otherwise. *) +val lift2 : ('a -> 'b -> 'c) -> 'a option -> 'b option -> 'c option diff --git a/lib/util.ml b/lib/util.ml index 3b5c90b02..389d0e129 100644 --- a/lib/util.ml +++ b/lib/util.ml @@ -790,43 +790,18 @@ let interval n m = let in_some x = Some x -let out_some = function - | Some x -> x - | None -> failwith "out_some" - -let option_map f = function - | None -> None - | Some x -> Some (f x) - let option_cons a l = match a with | Some x -> x::l | None -> l let option_fold_left2 f e a b = match (a,b) with | Some x, Some y -> f e x y - | _ -> e - -let option_fold_left f e a = match a with - | Some x -> f e x - | _ -> e - -let option_fold_right f a e = match a with - | Some x -> f x e - | _ -> e let option_compare f a b = match (a,b) with | None, None -> true | Some a', Some b' -> f a' b' | _ -> failwith "option_compare" -let option_iter f = function - | None -> () - | Some x -> f x - -let option_smartmap f a = match a with - | None -> a - | Some x -> let x' = f x in if x'==x then a else Some x' - let rec filter_some = function | [] -> [] | None::l -> filter_some l diff --git a/lib/util.mli b/lib/util.mli index 5e89788b9..0282f45f5 100644 --- a/lib/util.mli +++ b/lib/util.mli @@ -224,16 +224,10 @@ val intmap_inv : 'a Intmap.t -> 'a -> int list val interval : int -> int -> int list val in_some : 'a -> 'a option -val out_some : 'a option -> 'a -val option_map : ('a -> 'b) -> 'a option -> 'b option val option_cons : 'a option -> 'a list -> 'a list -val option_fold_right : ('a -> 'b -> 'b) -> 'a option -> 'b -> 'b -val option_fold_left : ('a -> 'b -> 'a) -> 'a -> 'b option -> 'a val option_fold_left2 : ('a -> 'b -> 'c -> 'a) -> 'a -> 'b option -> 'c option -> 'a -val option_iter : ('a -> unit) -> 'a option -> unit val option_compare : ('a -> 'b -> bool) -> 'a option -> 'b option -> bool -val option_smartmap : ('a -> 'a) -> 'a option -> 'a option val filter_some : 'a option list -> 'a list (* In [map_succeed f l] an element [a] is removed if [f a] raises *) 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 diff --git a/parsing/egrammar.ml b/parsing/egrammar.ml index e28890cee..b2c279b39 100644 --- a/parsing/egrammar.ml +++ b/parsing/egrammar.ml @@ -160,7 +160,7 @@ type grammar_tactic_production = let make_prod_item = function | TacTerm s -> (Gramext.Stoken (Lexer.terminal s), None) - | TacNonTerm (_,(nont,t), po) -> (nont, option_map (fun p -> (p,t)) po) + | TacNonTerm (_,(nont,t), po) -> (nont, Option.map (fun p -> (p,t)) po) (* Tactic grammar extensions *) @@ -194,7 +194,7 @@ let extend_vernac_command_grammar s gl = let find_index s t = let t,n = repr_ident (id_of_string t) in if s <> t or n = None then raise Not_found; - out_some n + Option.get n let rec interp_entry_name up_level s = let l = String.length s in @@ -233,7 +233,7 @@ let make_vprod_item n = function | VTerm s -> (Gramext.Stoken (Lexer.terminal s), None) | VNonTerm (loc, nt, po) -> let (etyp, e) = interp_entry_name n nt in - e, option_map (fun p -> (p,etyp)) po + e, Option.map (fun p -> (p,etyp)) po let get_tactic_entry n = if n = 0 then diff --git a/parsing/g_ascii_syntax.ml b/parsing/g_ascii_syntax.ml index ac54fc63d..717abaa66 100644 --- a/parsing/g_ascii_syntax.ml +++ b/parsing/g_ascii_syntax.ml @@ -72,7 +72,7 @@ let make_ascii_string n = if n>=32 && n<=126 then String.make 1 (char_of_int n) else Printf.sprintf "%03d" n -let uninterp_ascii_string r = option_map make_ascii_string (uninterp_ascii r) +let uninterp_ascii_string r = Option.map make_ascii_string (uninterp_ascii r) let _ = Notation.declare_string_interpreter "char_scope" diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4 index 04e0f84ca..4627d2305 100644 --- a/parsing/g_constr.ml4 +++ b/parsing/g_constr.ml4 @@ -59,7 +59,7 @@ let mk_fixb (id,bl,ann,body,(loc,tyc)) = (snd id,(n,ro),bl,ty,body) let mk_cofixb (id,bl,ann,body,(loc,tyc)) = - let _ = option_map (fun (aloc,_) -> + let _ = Option.map (fun (aloc,_) -> Util.user_err_loc (aloc,"Constr:mk_cofixb", Pp.str"Annotation forbidden in cofix expression")) (fst ann) in diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4 index 9b21837d8..23e4ba621 100644 --- a/parsing/g_tactic.ml4 +++ b/parsing/g_tactic.ml4 @@ -104,7 +104,7 @@ let mk_fix_tac (loc,id,bl,ann,ty) = (id,n,CProdN(loc,bl,ty)) let mk_cofix_tac (loc,id,bl,ann,ty) = - let _ = option_map (fun (aloc,_) -> + let _ = Option.map (fun (aloc,_) -> Util.user_err_loc (aloc,"Constr:mk_cofix_tac", Pp.str"Annotation forbidden in cofix expression")) ann in diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index a64cf74cc..a7a78f770 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -274,8 +274,8 @@ GEXTEND Gram ; rec_annotation: [ [ "{"; IDENT "struct"; id=IDENT; "}" -> (Some (id_of_string id), CStructRec) - | "{"; IDENT "wf"; rel=constr; id=OPT IDENT; "}" -> (option_map id_of_string id, CWfRec rel) - | "{"; IDENT "measure"; rel=constr; id=OPT IDENT; "}" -> (option_map id_of_string id, CMeasureRec rel) + | "{"; IDENT "wf"; rel=constr; id=OPT IDENT; "}" -> (Option.map id_of_string id, CWfRec rel) + | "{"; IDENT "measure"; rel=constr; id=OPT IDENT; "}" -> (Option.map id_of_string id, CMeasureRec rel) | -> (None, CStructRec) ] ] ; diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4 index d72a49046..07055869a 100644 --- a/parsing/pcoq.ml4 +++ b/parsing/pcoq.ml4 @@ -576,7 +576,7 @@ let find_position forpat other assoc lev = | (p,_ as pa)::l when p > n -> pa :: add_level (Some p) l | (p,a)::l when p = n -> if admissible_assoc (a,assoc) then raise Exit; - error_level_assoc p a (out_some assoc) + error_level_assoc p a (Option.get assoc) | l -> after := q; (n,create_assoc assoc)::l in try @@ -587,7 +587,7 @@ let find_position forpat other assoc lev = level_stack := updated:: !level_stack; let assoc = create_assoc assoc in (if !after = None then Some Gramext.First - else Some (Gramext.After (constr_level (out_some !after)))), + else Some (Gramext.After (constr_level (Option.get !after)))), Some assoc, Some (constr_level n) with Exit -> diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml index 1c9eb1e2a..8e542ce14 100644 --- a/parsing/ppconstr.ml +++ b/parsing/ppconstr.ml @@ -386,12 +386,12 @@ let pr_fixdecl pr prd dangling_with_for (id,(n,ro),bl,t,c) = match ro with CStructRec -> if List.length ids > 1 && n <> None then - spc() ++ str "{struct " ++ pr_name (snd (List.nth ids (out_some n))) ++ str"}" + spc() ++ str "{struct " ++ pr_name (snd (List.nth ids (Option.get n))) ++ str"}" else mt() | CWfRec c -> - spc () ++ str "{wf " ++ pr lsimple c ++ pr_name (snd (List.nth ids (out_some n))) ++ str"}" + spc () ++ str "{wf " ++ pr lsimple c ++ pr_name (snd (List.nth ids (Option.get n))) ++ str"}" | CMeasureRec c -> - spc () ++ str "{measure " ++ pr lsimple c ++ pr_name (snd (List.nth ids (out_some n))) ++ str"}" + spc () ++ str "{measure " ++ pr lsimple c ++ pr_name (snd (List.nth ids (Option.get n))) ++ str"}" in pr_recursive_decl pr prd dangling_with_for id bl annot t c @@ -428,7 +428,7 @@ let pr_case_item pr (tm,(na,indnalopt)) = | Name id when not (is_var id tm) -> spc () ++ str "as " ++ pr_id id | Anonymous when tm_clash (tm,indnalopt) <> None -> (* hide [tm] name to avoid conflicts *) - spc () ++ str "as _" (* ++ pr_id (out_some (tm_clash (tm,indnalopt)))*) + spc () ++ str "as _" (* ++ pr_id (Option.get (tm_clash (tm,indnalopt)))*) | _ -> mt ()) ++ *) (match na with (* Decision of printing "_" or not moved to constrextern.ml *) diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml index a5bcea6f1..bbb481f3e 100644 --- a/parsing/ppvernac.ml +++ b/parsing/ppvernac.ml @@ -747,7 +747,7 @@ let rec pr_vernac = function prlist (function None -> str " _" | Some id -> spc () ++ pr_id id) idl ++ str" :=" ++ brk(1,1) ++ - let idl = List.map out_some (List.filter (fun x -> not (x=None)) idl)in + let idl = List.map Option.get (List.filter (fun x -> not (x=None)) idl)in pr_raw_tactic_env (idl @ List.map snd (List.map fst l)) (Global.env()) @@ -794,7 +794,7 @@ let rec pr_vernac = function spc() ++ str"in" ++ spc () ++ pr_constr c) | None -> hov 2 (str"Check" ++ spc() ++ pr_constr c) in - (if io = None then mt() else int (out_some io) ++ str ": ") ++ + (if io = None then mt() else int (Option.get io) ++ str ": ") ++ pr_mayeval r c | VernacGlobalCheck c -> hov 2 (str"Type" ++ pr_constrarg c) | VernacPrint p -> diff --git a/parsing/prettyp.ml b/parsing/prettyp.ml index a2341edb1..a3a0c2f15 100644 --- a/parsing/prettyp.ml +++ b/parsing/prettyp.ml @@ -456,10 +456,10 @@ let gallina_print_leaf_entry with_values c = let gallina_print_context with_values = let rec prec n = function - | h::rest when n = None or out_some n > 0 -> + | h::rest when n = None or Option.get n > 0 -> (match gallina_print_library_entry with_values h with | None -> prec n rest - | Some pp -> prec (option_map ((+) (-1)) n) rest ++ pp ++ fnl ()) + | Some pp -> prec (Option.map ((+) (-1)) n) rest ++ pp ++ fnl ()) | _ -> mt () in prec diff --git a/parsing/search.ml b/parsing/search.ml index b9982ad3d..fd9eb12bb 100644 --- a/parsing/search.ml +++ b/parsing/search.ml @@ -52,7 +52,7 @@ let gen_crible refopt (fn : global_reference -> env -> constr -> unit) = (try let (idc,_,typ) = get_variable (basename sp) in if refopt = None - || head_const typ = constr_of_global (out_some refopt) + || head_const typ = constr_of_global (Option.get refopt) then fn (VarRef idc) env typ with Not_found -> (* we are in a section *) ()) @@ -60,7 +60,7 @@ let gen_crible refopt (fn : global_reference -> env -> constr -> unit) = let cst = locate_constant (qualid_of_sp sp) in let typ = Typeops.type_of_constant env cst in if refopt = None - || head_const typ = constr_of_global (out_some refopt) + || head_const typ = constr_of_global (Option.get refopt) then fn (ConstRef cst) env typ | "INDUCTIVE" -> diff --git a/pretyping/cases.ml b/pretyping/cases.ml index fd8f24370..058f3d210 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -421,7 +421,7 @@ let mkDeclTomatch na = function let map_tomatch_type f = function | IsInd (t,ind) -> IsInd (f t,map_inductive_type f ind) - | NotInd (c,t) -> NotInd (option_map f c, f t) + | NotInd (c,t) -> NotInd (Option.map f c, f t) let liftn_tomatch_type n depth = map_tomatch_type (liftn n depth) let lift_tomatch_type n = liftn_tomatch_type n 1 @@ -1139,7 +1139,7 @@ let rec generalize_problem pb = function let tomatch = regeneralize_index_tomatch (i+1) tomatch in { pb with tomatch = Abstract d :: tomatch; - pred = option_map (generalize_predicate i d) pb'.pred } + pred = Option.map (generalize_predicate i d) pb'.pred } (* No more patterns: typing the right-hand-side of equations *) let build_leaf pb = @@ -1154,7 +1154,7 @@ let build_leaf pb = let shift_problem (current,t) pb = {pb with tomatch = Alias (current,current,NonDepAlias,type_of_tomatch t)::pb.tomatch; - pred = option_map (specialize_predicate_var (current,t)) pb.pred; + pred = Option.map (specialize_predicate_var (current,t)) pb.pred; history = push_history_pattern 0 AliasLeaf pb.history; mat = List.map remove_current_pattern pb.mat } @@ -1224,7 +1224,7 @@ let build_branch current deps pb eqns const_info = { pb with env = push_rels sign pb.env; tomatch = List.rev_append currents tomatch; - pred = option_map (specialize_predicate (List.rev typs') dep_sign const_info) pb.pred; + pred = Option.map (specialize_predicate (List.rev typs') dep_sign const_info) pb.pred; history = history; mat = List.map (push_rels_eqn_with_names sign) submat } @@ -1291,7 +1291,7 @@ and compile_generalization pb d rest = { pb with env = push_rel d pb.env; tomatch = rest; - pred = option_map ungeneralize_predicate pb.pred; + pred = Option.map ungeneralize_predicate pb.pred; mat = List.map (push_rels_eqn [d]) pb.mat } in let j = compile pb in { uj_val = mkLambda_or_LetIn d j.uj_val; @@ -1316,7 +1316,7 @@ and compile_alias pb (deppat,nondeppat,d,t) rest = {pb with env = newenv; tomatch = tomatch; - pred = option_map (lift_predicate n) pb.pred; + pred = Option.map (lift_predicate n) pb.pred; history = history; mat = mat } in let j = compile pb in @@ -1500,7 +1500,7 @@ let extract_arity_signature env0 tomatchl tmsign = match tm with | NotInd (bo,typ) -> (match t with - | None -> [na,option_map (lift n) bo,lift n typ] + | None -> [na,Option.map (lift n) bo,lift n typ] | Some (loc,_,_,_) -> user_err_loc (loc,"", str "Unexpected type annotation for a term of non inductive type")) @@ -1566,7 +1566,7 @@ let prepare_predicate loc typing_fun evdref env tomatchs sign tycon = function let allnames = List.rev (List.map (List.map pi1) arsign) in let predcclj = typing_fun (mk_tycon (new_Type ())) env rtntyp in let _ = - option_map (fun tycon -> + Option.map (fun tycon -> evdref := Coercion.inh_conv_coerces_to loc env !evdref predcclj.uj_val (lift_tycon_type (List.length arsign) tycon)) tycon diff --git a/pretyping/clenv.ml b/pretyping/clenv.ml index dbc51514c..b9881aaf0 100644 --- a/pretyping/clenv.ml +++ b/pretyping/clenv.ml @@ -106,7 +106,7 @@ let clenv_environments evd bound t = let dep = dependent (mkRel 1) t2 in let na' = if dep then na else Anonymous in let e' = meta_declare mv t1 ~name:na' e in - clrec (e', (mkMeta mv)::metas) (option_map ((+) (-1)) n) + clrec (e', (mkMeta mv)::metas) (Option.map ((+) (-1)) n) (if dep then (subst1 (mkMeta mv) t2) else t2) | (n, LetIn (na,b,_,t)) -> clrec (e,metas) n (subst1 b t) | (n, _) -> (e, List.rev metas, t) @@ -124,7 +124,7 @@ let clenv_environments_evars env evd bound t = | (n, Prod (na,t1,t2)) -> let e',constr = Evarutil.new_evar e env t1 in let dep = dependent (mkRel 1) t2 in - clrec (e', constr::ts) (option_map ((+) (-1)) n) + clrec (e', constr::ts) (Option.map ((+) (-1)) n) (if dep then (subst1 constr t2) else t2) | (n, LetIn (na,b,_,t)) -> clrec (e,ts) n (subst1 b t) | (n, _) -> (e, List.rev ts, t) diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml index 62e29dc06..f3468bcbf 100644 --- a/pretyping/coercion.ml +++ b/pretyping/coercion.ml @@ -184,7 +184,7 @@ module Default = struct kind_of_term (whd_betadeltaiota env (evars_of evd) c1) with | Prod (_,t1,t2), Prod (name,u1,u2) -> - let v' = option_map (whd_betadeltaiota env (evars_of evd)) v in + let v' = Option.map (whd_betadeltaiota env (evars_of evd)) v in let (evd',b) = match v' with | Some v' -> @@ -201,7 +201,7 @@ module Default = struct let env1 = push_rel (x,None,v1) env in let (evd'', v2', t2') = inh_conv_coerce_to_fail loc env1 evd' (Some v2) t2 u2 in - (evd'', option_map (fun v2' -> mkLambda (x, v1, v2')) v2', + (evd'', Option.map (fun v2' -> mkLambda (x, v1, v2')) v2', mkProd (x, v1, t2')) | None -> (* Mismatch on t1 and u1 or not a lambda: we eta-expand *) @@ -219,7 +219,7 @@ module Default = struct let (evd'', v2', t2') = let v2 = match v with - | Some v -> option_map (fun x -> mkApp(lift 1 v,[|x|])) v1' + | Some v -> Option.map (fun x -> mkApp(lift 1 v,[|x|])) v1' | None -> None and evd', t2 = match v1' with @@ -231,7 +231,7 @@ module Default = struct in inh_conv_coerce_to_fail loc env1 evd' v2 t2 u2 in - (evd'', option_map (fun v2' -> mkLambda (name, u1, v2')) v2', + (evd'', Option.map (fun v2' -> mkLambda (name, u1, v2')) v2', mkProd (name, u1, t2'))) | _ -> raise NoCoercion diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index 829c5f404..9dfe393be 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -303,7 +303,7 @@ let detype_case computable detype detype_eqns testdep avoid data p c bl = then Anonymous, None, None else - match option_map detype p with + match Option.map detype p with | None -> Anonymous, None, None | Some p -> let nl,typ = it_destRLambda_or_LetIn_names k p in @@ -340,7 +340,7 @@ let detype_case computable detype detype_eqns testdep avoid data p c bl = array_map3 (extract_nondep_branches testdep) bl bl' consnargsl in if array_for_all ((<>) None) nondepbrs then RIf (dl,tomatch,(alias,pred), - out_some nondepbrs.(0),out_some nondepbrs.(1)) + Option.get nondepbrs.(0),Option.get nondepbrs.(1)) else RCases (dl,pred,[tomatch,(alias,aliastyp)],eqnl) | _ -> @@ -529,7 +529,7 @@ and detype_binder isgoal bk avoid env na ty c = | BLetIn -> RLetIn (dl, na',detype isgoal avoid env ty, r) let rec detype_rel_context where avoid env sign = - let where = option_map (fun c -> it_mkLambda_or_LetIn c sign) where in + let where = Option.map (fun c -> it_mkLambda_or_LetIn c sign) where in let rec aux avoid env = function | [] -> [] | (na,b,t)::rest -> @@ -539,7 +539,7 @@ let rec detype_rel_context where avoid env sign = | Some c -> if b<>None then concrete_let_name None avoid env na c else concrete_name None avoid env na c in - let b = option_map (detype false avoid env) b in + let b = Option.map (detype false avoid env) b in let t = detype false avoid env t in (na',b,t) :: aux avoid' (add_name na' env) rest in aux avoid env (List.rev sign) @@ -589,11 +589,11 @@ let rec subst_rawconstr subst raw = RLetIn (loc,n,r1',r2') | RCases (loc,rtno,rl,branches) -> - let rtno' = option_smartmap (subst_rawconstr subst) rtno + let rtno' = Option.smartmap (subst_rawconstr subst) rtno and rl' = list_smartmap (fun (a,x as y) -> let a' = subst_rawconstr subst a in let (n,topt) = x in - let topt' = option_smartmap + let topt' = Option.smartmap (fun (loc,(sp,i),x,y as t) -> let sp' = subst_kn subst sp in if sp == sp' then t else (loc,(sp',i),x,y)) topt in @@ -611,14 +611,14 @@ let rec subst_rawconstr subst raw = RCases (loc,rtno',rl',branches') | RLetTuple (loc,nal,(na,po),b,c) -> - let po' = option_smartmap (subst_rawconstr subst) po + let po' = Option.smartmap (subst_rawconstr subst) po and b' = subst_rawconstr subst b and c' = subst_rawconstr subst c in if po' == po && b' == b && c' == c then raw else RLetTuple (loc,nal,(na,po'),b',c') | RIf (loc,c,(na,po),b1,b2) -> - let po' = option_smartmap (subst_rawconstr subst) po + let po' = Option.smartmap (subst_rawconstr subst) po and b1' = subst_rawconstr subst b1 and b2' = subst_rawconstr subst b2 and c' = subst_rawconstr subst c in @@ -631,7 +631,7 @@ let rec subst_rawconstr subst raw = let bl' = array_smartmap (list_smartmap (fun (na,obd,ty as dcl) -> let ty' = subst_rawconstr subst ty in - let obd' = option_smartmap (subst_rawconstr subst) obd in + let obd' = Option.smartmap (subst_rawconstr subst) obd in if ty'==ty & obd'==obd then dcl else (na,obd',ty'))) bl in if ra1' == ra1 && ra2' == ra2 && bl'==bl then raw else diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 9d0ae75e7..93e1c1157 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -43,7 +43,7 @@ let eval_flexible_term env c = match kind_of_term c with | Const c -> constant_opt_value env c | Rel n -> - (try let (_,v,_) = lookup_rel n env in option_map (lift n) v + (try let (_,v,_) = lookup_rel n env in Option.map (lift n) v with Not_found -> None) | Var id -> (try let (_,v,_) = lookup_named id env in v with Not_found -> None) diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml index cb64fcb56..1f256b3bd 100644 --- a/pretyping/evarutil.ml +++ b/pretyping/evarutil.ml @@ -226,7 +226,7 @@ let push_rel_context_to_named_context env typ = Sign.fold_rel_context (fun (na,c,t) (subst, avoid, env) -> let id = next_name_away na avoid in - let d = (id,option_map (substl subst) c,substl subst t) in + let d = (id,Option.map (substl subst) c,substl subst t) in (mkVar id :: subst, id::avoid, push_named d env)) (rel_context env) ~init:([], ids, env) in (named_context_val env, substl subst typ, inst_rels@inst_vars) @@ -1133,7 +1133,7 @@ let lift_abstr_tycon_type n (abs, t) = else (Some (init, abs'), t) let lift_tycon_type n (abs, t) = (abs, lift n t) -let lift_tycon n = option_map (lift_tycon_type n) +let lift_tycon n = Option.map (lift_tycon_type n) let pr_tycon_type env (abs, t) = match abs with diff --git a/pretyping/evd.ml b/pretyping/evd.ml index d0cbeb574..6d75dada6 100644 --- a/pretyping/evd.ml +++ b/pretyping/evd.ml @@ -430,7 +430,7 @@ let evar_declare hyps evk ty ?(src=(dummy_loc,InternalHole)) ?filter evd = if filter = None then List.map (fun _ -> true) (named_context_of_val hyps) else - (let filter = out_some filter in + (let filter = Option.get filter in assert (List.length filter = List.length (named_context_of_val hyps)); filter) in diff --git a/pretyping/matching.ml b/pretyping/matching.ml index cac06d240..9ce8e703f 100644 --- a/pretyping/matching.ml +++ b/pretyping/matching.ml @@ -153,7 +153,7 @@ let matches_core convert allow_partial_app pat c = sorec ((na2,t2)::stk) (sorec stk sigma c1 c2) d1 d2 | PRef (ConstRef _ as ref), _ when convert <> None -> - let (env,evars) = out_some convert in + let (env,evars) = Option.get convert in let c = constr_of_global ref in if is_conv env evars c cT then sigma else raise PatternMatchingFailure diff --git a/pretyping/pattern.ml b/pretyping/pattern.ml index c3b49b974..d64e84fea 100644 --- a/pretyping/pattern.ml +++ b/pretyping/pattern.ml @@ -185,7 +185,7 @@ let rec subst_pattern subst pat = match pat with if c' == c && c1' == c1 && c2' == c2 then pat else PIf (c',c1',c2') | PCase ((a,b,ind,n as cs),typ,c,branches) -> - let ind' = option_smartmap (Inductiveops.subst_inductive subst) ind in + let ind' = Option.smartmap (Inductiveops.subst_inductive subst) ind in let typ' = subst_pattern subst typ in let c' = subst_pattern subst c in let branches' = array_smartmap (subst_pattern subst) branches in diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml index 26ccc8024..ad4e06a55 100644 --- a/pretyping/pretype_errors.ml +++ b/pretyping/pretype_errors.ml @@ -60,7 +60,7 @@ let env_ise sigma env = Sign.fold_rel_context (fun (na,b,ty) e -> push_rel - (na, option_map (nf_evar sigma) b, nf_evar sigma ty) + (na, Option.map (nf_evar sigma) b, nf_evar sigma ty) e) ctxt ~init:env0 @@ -76,7 +76,7 @@ let contract env lc = env | _ -> let t' = substl !l t in - let c' = option_map (substl !l) c in + let c' = Option.map (substl !l) c in let na' = named_hd env t' na in l := (mkRel 1) :: List.map (lift 1) !l; push_rel (na',c',t') env in diff --git a/pretyping/rawterm.ml b/pretyping/rawterm.ml index 63e40a052..d2a347363 100644 --- a/pretyping/rawterm.ml +++ b/pretyping/rawterm.ml @@ -101,7 +101,7 @@ let cases_predicate_names tml = - boolean in POldCase means it is recursive i*) -let map_rawdecl f (na,obd,ty) = (na,option_map f obd,f ty) +let map_rawdecl f (na,obd,ty) = (na,Option.map f obd,f ty) let map_rawconstr f = function | RVar (loc,id) -> RVar (loc,id) @@ -110,13 +110,13 @@ let map_rawconstr f = function | RProd (loc,na,ty,c) -> RProd (loc,na,f ty,f c) | RLetIn (loc,na,b,c) -> RLetIn (loc,na,f b,f c) | RCases (loc,rtntypopt,tml,pl) -> - RCases (loc,option_map f rtntypopt, + RCases (loc,Option.map f rtntypopt, List.map (fun (tm,x) -> (f tm,x)) tml, List.map (fun (loc,idl,p,c) -> (loc,idl,p,f c)) pl) | RLetTuple (loc,nal,(na,po),b,c) -> - RLetTuple (loc,nal,(na,option_map f po),f b,f c) + RLetTuple (loc,nal,(na,Option.map f po),f b,f c) | RIf (loc,c,(na,po),b1,b2) -> - RIf (loc,f c,(na,option_map f po),f b1,f b2) + RIf (loc,f c,(na,Option.map f po),f b1,f b2) | RRec (loc,fk,idl,bl,tyl,bv) -> RRec (loc,fk,idl,Array.map (List.map (map_rawdecl f)) bl, Array.map f tyl,Array.map f bv) @@ -149,7 +149,7 @@ let map_rawconstr_with_binders_loc loc g f e = function let g' id e = snd (g id e) in let h (_,idl,p,c) = (loc,idl,p,f (List.fold_right g' idl e) c) in RCases - (loc,option_map (f e) tyopt,List.map (f e) tml, List.map h pl) + (loc,Option.map (f e) tyopt,List.map (f e) tml, List.map h pl) | RRec (_,fk,idl,tyl,bv) -> let idl',e' = fold_ident g idl e in RRec (loc,fk,idl',Array.map (f e) tyl,Array.map (f e') bv) diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml index 8ca06e9a5..4b93388d6 100644 --- a/pretyping/recordops.ml +++ b/pretyping/recordops.ml @@ -40,15 +40,13 @@ type struc_typ = { let structure_table = ref (Indmap.empty : struc_typ Indmap.t) let projection_table = ref Cmap.empty -let option_fold_right f p e = match p with Some a -> f a e | None -> e - let load_structure i (_,(ind,id,kl,projs)) = let n = (fst (Global.lookup_inductive ind)).Declarations.mind_nparams in let struc = { s_CONST = id; s_EXPECTEDPARAM = n; s_PROJ = projs; s_PROJKIND = kl } in structure_table := Indmap.add ind struc !structure_table; projection_table := - List.fold_right (option_fold_right (fun proj -> Cmap.add proj struc)) + List.fold_right (Option.fold_right (fun proj -> Cmap.add proj struc)) projs !projection_table let cache_structure o = @@ -60,7 +58,7 @@ let subst_structure (_,subst,((kn,i),id,kl,projs as obj)) = (* invariant: struc.s_PROJ is an evaluable reference. Thus we can take *) (* the first component of subst_con. *) list_smartmap - (option_smartmap (fun kn -> fst (subst_con subst kn))) + (Option.smartmap (fun kn -> fst (subst_con subst kn))) projs in if projs' == projs && kn' == kn then obj else @@ -68,7 +66,7 @@ let subst_structure (_,subst,((kn,i),id,kl,projs as obj)) = let discharge_structure (_,(ind,id,kl,projs)) = Some (Lib.discharge_inductive ind, id, kl, - List.map (option_map Lib.discharge_con) projs) + List.map (Option.map Lib.discharge_con) projs) let (inStruc,outStruc) = declare_object {(default_object "STRUCTURE") with 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 diff --git a/tactics/auto.ml b/tactics/auto.ml index a3ac17b34..8bce850db 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -297,7 +297,7 @@ let subst_autohint (_,subst,(local,name,hintlist as obj)) = let trans_clenv clenv = Clenv.subst_clenv subst clenv in let trans_data data code = { data with - pat = option_smartmap (subst_pattern subst) data.pat ; + pat = Option.smartmap (subst_pattern subst) data.pat ; code = code ; } in @@ -637,7 +637,7 @@ and my_find_search db_list local_db hdc concl = (trivial_fail_db db_list local_db) | Unfold_nth c -> unfold_in_concl [[],c] | Extern tacast -> - conclPattern concl (out_some p) tacast)) + conclPattern concl (Option.get p) tacast)) tacl and trivial_resolve db_list local_db cl = @@ -781,7 +781,7 @@ let gen_auto n lems dbnames = | None -> full_auto n lems | Some l -> auto n lems l -let inj_or_var = option_map (fun n -> ArgArg n) +let inj_or_var = Option.map (fun n -> ArgArg n) let h_auto n lems l = Refiner.abstract_tactic (TacAuto (inj_or_var n,List.map inj_open lems,l)) diff --git a/tactics/decl_interp.ml b/tactics/decl_interp.ml index ec8a38501..771dbe736 100644 --- a/tactics/decl_interp.ml +++ b/tactics/decl_interp.ml @@ -25,10 +25,10 @@ open Pp let raw_app (loc,hd,args) = if args =[] then hd else RApp(loc,hd,args) let intern_justification_items globs = - option_map (List.map (intern_constr globs)) + Option.map (List.map (intern_constr globs)) let intern_justification_method globs = - option_map (intern_tactic globs) + Option.map (intern_tactic globs) let intern_statement intern_it globs st = {st_label=st.st_label; @@ -52,7 +52,7 @@ let add_name nam globs= let intern_hyp iconstr globs = function Hvar (loc,(id,topt)) -> add_var id globs, - Hvar (loc,(id,option_map (intern_constr globs) topt)) + Hvar (loc,(id,Option.map (intern_constr globs) topt)) | Hprop st -> add_name st.st_label globs, Hprop (intern_statement iconstr globs st) @@ -73,7 +73,7 @@ let intern_casee globs = function let intern_hyp_list args globs = let intern_one globs (loc,(id,opttyp)) = (add_var id globs), - (loc,(id,option_map (intern_constr globs) opttyp)) in + (loc,(id,Option.map (intern_constr globs) opttyp)) in list_fold_map intern_one globs args let intern_suffices_clause globs (hyps,c) = @@ -141,7 +141,7 @@ let rec intern_proof_instr globs instr= (* INTERP *) let interp_justification_items sigma env = - option_map (List.map (fun c ->understand sigma env (fst c))) + Option.map (List.map (fun c ->understand sigma env (fst c))) let interp_constr check_sort sigma env c = if check_sort then diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4 index b62bf5820..7a6b07d38 100644 --- a/tactics/eauto.ml4 +++ b/tactics/eauto.ml4 @@ -94,7 +94,7 @@ let e_split = e_constructor_tac (Some 1) 1 TACTIC EXTEND econstructor [ "econstructor" integer(n) "with" bindings(c) ] -> [ e_constructor_tac None n c ] | [ "econstructor" integer(n) ] -> [ e_constructor_tac None n NoBindings ] -| [ "econstructor" tactic_opt(t) ] -> [ e_any_constructor (option_map Tacinterp.eval_tactic t) ] +| [ "econstructor" tactic_opt(t) ] -> [ e_any_constructor (Option.map Tacinterp.eval_tactic t) ] END TACTIC EXTEND eleft @@ -192,7 +192,7 @@ and e_my_find_search db_list local_db hdc concl = (e_trivial_fail_db db_list local_db) | Unfold_nth c -> unfold_in_concl [[],c] | Extern tacast -> conclPattern concl - (out_some p) tacast + (Option.get p) tacast in (tac,fmt_autotactic t)) (*i diff --git a/tactics/extraargs.ml4 b/tactics/extraargs.ml4 index 4a6c2ffb2..48d4afbc1 100644 --- a/tactics/extraargs.ml4 +++ b/tactics/extraargs.ml4 @@ -221,7 +221,7 @@ END let gen_in_arg_hyp_to_clause trad_id (hyps ,concl) : Tacticals.clause = {Tacexpr.onhyps= - Util.option_map + Option.map (fun l -> List.map (fun id -> ( ([],trad_id id) ,Tacexpr.InHyp)) diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4 index 787847400..3ddb4188b 100644 --- a/tactics/extratactics.ml4 +++ b/tactics/extratactics.ml4 @@ -23,7 +23,7 @@ open Equality TACTIC EXTEND replace ["replace" constr(c1) "with" constr(c2) in_arg_hyp(in_hyp) by_arg_tac(tac) ] --> [ replace_in_clause_maybe_by c1 c2 (glob_in_arg_hyp_to_clause in_hyp) (Util.option_map Tacinterp.eval_tactic tac) ] +-> [ replace_in_clause_maybe_by c1 c2 (glob_in_arg_hyp_to_clause in_hyp) (Option.map Tacinterp.eval_tactic tac) ] END TACTIC EXTEND replace_term_left @@ -152,21 +152,21 @@ open Setoid_replace TACTIC EXTEND setoid_replace [ "setoid_replace" constr(c1) "with" constr(c2) by_arg_tac(tac)] -> - [ setoid_replace (Util.option_map Tacinterp.eval_tactic tac) None c1 c2 ~new_goals:[] ] + [ setoid_replace (Option.map Tacinterp.eval_tactic tac) None c1 c2 ~new_goals:[] ] | [ "setoid_replace" constr(c1) "with" constr(c2) "using" "relation" constr(rel) by_arg_tac(tac)] -> - [ setoid_replace (Util.option_map Tacinterp.eval_tactic tac) (Some rel) c1 c2 ~new_goals:[] ] + [ setoid_replace (Option.map Tacinterp.eval_tactic tac) (Some rel) c1 c2 ~new_goals:[] ] | [ "setoid_replace" constr(c1) "with" constr(c2) "generate" "side" "conditions" constr_list(l) by_arg_tac(tac) ] -> - [ setoid_replace (Util.option_map Tacinterp.eval_tactic tac) None c1 c2 ~new_goals:l ] + [ setoid_replace (Option.map Tacinterp.eval_tactic tac) None c1 c2 ~new_goals:l ] | [ "setoid_replace" constr(c1) "with" constr(c2) "using" "relation" constr(rel) "generate" "side" "conditions" constr_list(l) by_arg_tac(tac) ] -> - [ setoid_replace (Util.option_map Tacinterp.eval_tactic tac) (Some rel) c1 c2 ~new_goals:l ] + [ setoid_replace (Option.map Tacinterp.eval_tactic tac) (Some rel) c1 c2 ~new_goals:l ] | [ "setoid_replace" constr(c1) "with" constr(c2) "in" hyp(h) by_arg_tac(tac) ] -> - [ setoid_replace_in (Util.option_map Tacinterp.eval_tactic tac) h None c1 c2 ~new_goals:[] ] + [ setoid_replace_in (Option.map Tacinterp.eval_tactic tac) h None c1 c2 ~new_goals:[] ] | [ "setoid_replace" constr(c1) "with" constr(c2) "in" hyp(h) "using" "relation" constr(rel) by_arg_tac(tac)] -> - [ setoid_replace_in (Util.option_map Tacinterp.eval_tactic tac) h (Some rel) c1 c2 ~new_goals:[] ] + [ setoid_replace_in (Option.map Tacinterp.eval_tactic tac) h (Some rel) c1 c2 ~new_goals:[] ] | [ "setoid_replace" constr(c1) "with" constr(c2) "in" hyp(h) "generate" "side" "conditions" constr_list(l) by_arg_tac(tac)] -> - [ setoid_replace_in (Util.option_map Tacinterp.eval_tactic tac) h None c1 c2 ~new_goals:l ] + [ setoid_replace_in (Option.map Tacinterp.eval_tactic tac) h None c1 c2 ~new_goals:l ] | [ "setoid_replace" constr(c1) "with" constr(c2) "in" hyp(h) "using" "relation" constr(rel) "generate" "side" "conditions" constr_list(l) by_arg_tac(tac)] -> - [ setoid_replace_in (Util.option_map Tacinterp.eval_tactic tac) h (Some rel) c1 c2 ~new_goals:l ] + [ setoid_replace_in (Option.map Tacinterp.eval_tactic tac) h (Some rel) c1 c2 ~new_goals:l ] END TACTIC EXTEND setoid_rewrite diff --git a/tactics/hiddentac.ml b/tactics/hiddentac.ml index 8bb7c5c2c..f5c54a533 100644 --- a/tactics/hiddentac.ml +++ b/tactics/hiddentac.ml @@ -30,7 +30,7 @@ let inj_occ (occ,c) = (occ,inj_open c) (* Basic tactics *) let h_intro_move x y = - abstract_tactic (TacIntroMove (x, option_map inj_id y)) (intro_move x y) + abstract_tactic (TacIntroMove (x, Option.map inj_id y)) (intro_move x y) let h_intro x = h_intro_move (Some x) None let h_intros_until x = abstract_tactic (TacIntrosUntil x) (intros_until x) let h_assumption = abstract_tactic TacAssumption assumption @@ -43,7 +43,7 @@ let h_apply ev cb = abstract_tactic (TacApply (ev,inj_open_wb cb)) (apply_with_ebindings_gen ev cb) let h_elim ev cb cbo = - abstract_tactic (TacElim (ev,inj_open_wb cb,option_map inj_open_wb cbo)) + abstract_tactic (TacElim (ev,inj_open_wb cb,Option.map inj_open_wb cbo)) (elim ev cb cbo) let h_elim_type c = abstract_tactic (TacElimType (inj_open c)) (elim_type c) let h_case ev cb = abstract_tactic (TacCase (ev,inj_open_wb cb)) (general_case_analysis ev cb) @@ -78,10 +78,10 @@ let h_simple_induction h = let h_simple_destruct h = abstract_tactic (TacSimpleDestruct h) (simple_destruct h) let h_new_induction ev c e idl = - abstract_tactic (TacNewInduction (ev,List.map inj_ia c,option_map inj_open_wb e,idl)) + abstract_tactic (TacNewInduction (ev,List.map inj_ia c,Option.map inj_open_wb e,idl)) (new_induct ev c e idl) let h_new_destruct ev c e idl = - abstract_tactic (TacNewDestruct (ev,List.map inj_ia c,option_map inj_open_wb e,idl)) + abstract_tactic (TacNewDestruct (ev,List.map inj_ia c,Option.map inj_open_wb e,idl)) (new_destruct ev c e idl) let h_specialize n d = abstract_tactic (TacSpecialize (n,inj_open_wb d)) (new_hyp n d) let h_lapply c = abstract_tactic (TacLApply (inj_open c)) (cut_and_apply c) @@ -113,8 +113,8 @@ let h_simplest_right = h_right NoBindings let h_reduce r cl = abstract_tactic (TacReduce (inj_red_expr r,cl)) (reduce r cl) let h_change oc c cl = - abstract_tactic (TacChange (option_map inj_occ oc,inj_open c,cl)) - (change (option_map Redexpr.out_with_occurrences oc) c cl) + abstract_tactic (TacChange (Option.map inj_occ oc,inj_open c,cl)) + (change (Option.map Redexpr.out_with_occurrences oc) c cl) (* Equivalence relations *) let h_reflexivity = abstract_tactic TacReflexivity intros_reflexivity diff --git a/tactics/inv.ml b/tactics/inv.ml index bfaa7e5e4..d8d7661be 100644 --- a/tactics/inv.ml +++ b/tactics/inv.ml @@ -385,7 +385,7 @@ let rec get_names allow_conj = function | IntroOrAndPattern [l] -> if allow_conj then if l = [] then (None,[]) else - let l = List.map (fun id -> out_some (fst (get_names false id))) l in + let l = List.map (fun id -> Option.get (fst (get_names false id))) l in (Some (List.hd l), l) else error "Nested conjunctive patterns not allowed for inversion equations" diff --git a/tactics/nbtermdn.ml b/tactics/nbtermdn.ml index d53ca6126..c53a5088a 100644 --- a/tactics/nbtermdn.ml +++ b/tactics/nbtermdn.ml @@ -43,14 +43,14 @@ let get_dn dnm hkey = try Gmap.find hkey dnm with Not_found -> Btermdn.create () let add dn (na,(pat,valu)) = - let hkey = option_map fst (Termdn.constr_pat_discr pat) in + let hkey = Option.map fst (Termdn.constr_pat_discr pat) in dn.table <- Gmap.add na (pat,valu) dn.table; let dnm = dn.patterns in dn.patterns <- Gmap.add hkey (Btermdn.add (get_dn dnm hkey) (pat,valu)) dnm let rmv dn na = let (pat,valu) = Gmap.find na dn.table in - let hkey = option_map fst (Termdn.constr_pat_discr pat) in + let hkey = Option.map fst (Termdn.constr_pat_discr pat) in dn.table <- Gmap.remove na dn.table; let dnm = dn.patterns in dn.patterns <- Gmap.add hkey (Btermdn.rmv (get_dn dnm hkey) (pat,valu)) dnm @@ -62,7 +62,7 @@ let remap ndn na (pat,valu) = add ndn (na,(pat,valu)) let lookup dn valu = - let hkey = option_map fst (Termdn.constr_val_discr valu) in + let hkey = Option.map fst (Termdn.constr_val_discr valu) in try Btermdn.lookup (Gmap.find hkey dn.patterns) valu with Not_found -> [] let app f dn = Gmap.iter f dn.table diff --git a/tactics/setoid_replace.ml b/tactics/setoid_replace.ml index 36ef9be47..307968116 100644 --- a/tactics/setoid_replace.ml +++ b/tactics/setoid_replace.ml @@ -85,7 +85,7 @@ type morphism_class = let subst_mps_in_relation_class subst = function Relation t -> Relation (subst_mps subst t) - | Leibniz t -> Leibniz (option_map (subst_mps subst) t) + | Leibniz t -> Leibniz (Option.map (subst_mps subst) t) let subst_mps_in_argument_class subst (variance,rel) = variance, subst_mps_in_relation_class subst rel @@ -297,9 +297,9 @@ let relation_morphism_of_constr_morphism = let subst_relation subst relation = let rel_a' = subst_mps subst relation.rel_a in let rel_aeq' = subst_mps subst relation.rel_aeq in - let rel_refl' = option_map (subst_mps subst) relation.rel_refl in - let rel_sym' = option_map (subst_mps subst) relation.rel_sym in - let rel_trans' = option_map (subst_mps subst) relation.rel_trans in + let rel_refl' = Option.map (subst_mps subst) relation.rel_refl in + let rel_sym' = Option.map (subst_mps subst) relation.rel_sym in + let rel_trans' = Option.map (subst_mps subst) relation.rel_trans in let rel_X_relation_class' = subst_mps subst relation.rel_X_relation_class in let rel_Xreflexive_relation_class' = subst_mps subst relation.rel_Xreflexive_relation_class @@ -640,9 +640,9 @@ let apply_to_relation subst rel = assert (new_quantifiers_no >= 0) ; { rel_a = mkApp (rel.rel_a, subst) ; rel_aeq = mkApp (rel.rel_aeq, subst) ; - rel_refl = option_map (fun c -> mkApp (c,subst)) rel.rel_refl ; - rel_sym = option_map (fun c -> mkApp (c,subst)) rel.rel_sym; - rel_trans = option_map (fun c -> mkApp (c,subst)) rel.rel_trans; + rel_refl = Option.map (fun c -> mkApp (c,subst)) rel.rel_refl ; + rel_sym = Option.map (fun c -> mkApp (c,subst)) rel.rel_sym; + rel_trans = Option.map (fun c -> mkApp (c,subst)) rel.rel_trans; rel_quantifiers_no = new_quantifiers_no; rel_X_relation_class = mkApp (rel.rel_X_relation_class, subst); rel_Xreflexive_relation_class = @@ -1012,9 +1012,9 @@ let int_add_relation id a aeq refl sym trans = let env = Global.env () in let a_quantifiers_rev = check_a env a in check_eq env a_quantifiers_rev a aeq ; - option_iter (check_refl env a_quantifiers_rev a aeq) refl ; - option_iter (check_sym env a_quantifiers_rev a aeq) sym ; - option_iter (check_trans env a_quantifiers_rev a aeq) trans ; + Option.iter (check_refl env a_quantifiers_rev a aeq) refl ; + Option.iter (check_sym env a_quantifiers_rev a aeq) sym ; + Option.iter (check_trans env a_quantifiers_rev a aeq) trans ; let quantifiers_no = List.length a_quantifiers_rev in let aeq_rel = { rel_a = a; @@ -1075,9 +1075,9 @@ let int_add_relation id a aeq refl sym trans = let a_instance = apply_to_rels a a_quantifiers_rev in let aeq_instance = apply_to_rels aeq a_quantifiers_rev in let sym_instance = - option_map (fun x -> apply_to_rels x a_quantifiers_rev) sym in + Option.map (fun x -> apply_to_rels x a_quantifiers_rev) sym in let refl_instance = - option_map (fun x -> apply_to_rels x a_quantifiers_rev) refl in + Option.map (fun x -> apply_to_rels x a_quantifiers_rev) refl in let trans_instance = apply_to_rels trans a_quantifiers_rev in let aeq_rel_class_and_var1, aeq_rel_class_and_var2, lemma, output = match sym_instance, refl_instance with @@ -1132,8 +1132,8 @@ let int_add_relation id a aeq refl sym trans = (* The vernac command "Add Relation ..." *) let add_relation id a aeq refl sym trans = Coqlib.check_required_library ["Coq";"Setoids";"Setoid_tac"]; - int_add_relation id (constr_of a) (constr_of aeq) (option_map constr_of refl) - (option_map constr_of sym) (option_map constr_of trans) + int_add_relation id (constr_of a) (constr_of aeq) (Option.map constr_of refl) + (Option.map constr_of sym) (Option.map constr_of trans) (************************ Add Setoid ******************************************) diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 11d86630b..09d9fe8d7 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -550,7 +550,7 @@ let intern_red_expr ist = function | Cbv f -> Cbv (intern_flag ist f) | Lazy f -> Lazy (intern_flag ist f) | Pattern l -> Pattern (List.map (intern_constr_occurrence ist) l) - | Simpl o -> Simpl (option_map (intern_constr_occurrence ist) o) + | Simpl o -> Simpl (Option.map (intern_constr_occurrence ist) o) | (Red _ | Hnf | ExtraRedExpr _ | CbvVm as r ) -> r @@ -559,7 +559,7 @@ let intern_inversion_strength lf ist = function NonDepInversion (k,List.map (intern_hyp_or_metaid ist) idl, intern_intro_pattern lf ist ids) | DepInversion (k,copt,ids) -> - DepInversion (k, option_map (intern_constr ist) copt, + DepInversion (k, Option.map (intern_constr ist) copt, intern_intro_pattern lf ist ids) | InversionUsing (c,idl) -> InversionUsing (intern_constr ist c, List.map (intern_hyp_or_metaid ist) idl) @@ -654,8 +654,8 @@ let rec intern_atomic lf ist x = TacIntroPattern (List.map (intern_intro_pattern lf ist) l) | TacIntrosUntil hyp -> TacIntrosUntil (intern_quantified_hypothesis ist hyp) | TacIntroMove (ido,ido') -> - TacIntroMove (option_map (intern_ident lf ist) ido, - option_map (intern_hyp ist) ido') + TacIntroMove (Option.map (intern_ident lf ist) ido, + Option.map (intern_hyp ist) ido') | TacAssumption -> TacAssumption | TacExact c -> TacExact (intern_constr ist c) | TacExactNoCheck c -> TacExactNoCheck (intern_constr ist c) @@ -663,21 +663,21 @@ let rec intern_atomic lf ist x = | TacApply (ev,cb) -> TacApply (ev,intern_constr_with_bindings ist cb) | TacElim (ev,cb,cbo) -> TacElim (ev,intern_constr_with_bindings ist cb, - option_map (intern_constr_with_bindings ist) cbo) + Option.map (intern_constr_with_bindings ist) cbo) | TacElimType c -> TacElimType (intern_type ist c) | TacCase (ev,cb) -> TacCase (ev,intern_constr_with_bindings ist cb) | TacCaseType c -> TacCaseType (intern_type ist c) - | TacFix (idopt,n) -> TacFix (option_map (intern_ident lf ist) idopt,n) + | TacFix (idopt,n) -> TacFix (Option.map (intern_ident lf ist) idopt,n) | TacMutualFix (id,n,l) -> let f (id,n,c) = (intern_ident lf ist id,n,intern_type ist c) in TacMutualFix (intern_ident lf ist id, n, List.map f l) - | TacCofix idopt -> TacCofix (option_map (intern_ident lf ist) idopt) + | TacCofix idopt -> TacCofix (Option.map (intern_ident lf ist) idopt) | TacMutualCofix (id,l) -> let f (id,c) = (intern_ident lf ist id,intern_type ist c) in TacMutualCofix (intern_ident lf ist id, List.map f l) | TacCut c -> TacCut (intern_type ist c) | TacAssert (otac,ipat,c) -> - TacAssert (option_map (intern_tactic ist) otac, + TacAssert (Option.map (intern_tactic ist) otac, intern_intro_pattern lf ist ipat, intern_constr_gen (otac<>None) ist c) | TacGeneralize cl -> TacGeneralize (List.map (intern_constr ist) cl) @@ -690,14 +690,14 @@ let rec intern_atomic lf ist x = (* Automation tactics *) | TacTrivial (lems,l) -> TacTrivial (List.map (intern_constr ist) lems,l) | TacAuto (n,lems,l) -> - TacAuto (option_map (intern_or_var ist) n, + TacAuto (Option.map (intern_or_var ist) n, List.map (intern_constr ist) lems,l) | TacAutoTDB n -> TacAutoTDB n | TacDestructHyp (b,id) -> TacDestructHyp(b,intern_hyp ist id) | TacDestructConcl -> TacDestructConcl | TacSuperAuto (n,l,b1,b2) -> TacSuperAuto (n,l,b1,b2) | TacDAuto (n,p,lems) -> - TacDAuto (option_map (intern_or_var ist) n,p, + TacDAuto (Option.map (intern_or_var ist) n,p, List.map (intern_constr ist) lems) (* Derived basic tactics *) @@ -705,13 +705,13 @@ let rec intern_atomic lf ist x = TacSimpleInduction (intern_quantified_hypothesis ist h) | TacNewInduction (ev,lc,cbo,ids) -> TacNewInduction (ev,List.map (intern_induction_arg ist) lc, - option_map (intern_constr_with_bindings ist) cbo, + Option.map (intern_constr_with_bindings ist) cbo, (intern_intro_pattern lf ist ids)) | TacSimpleDestruct h -> TacSimpleDestruct (intern_quantified_hypothesis ist h) | TacNewDestruct (ev,c,cbo,ids) -> TacNewDestruct (ev,List.map (intern_induction_arg ist) c, - option_map (intern_constr_with_bindings ist) cbo, + Option.map (intern_constr_with_bindings ist) cbo, (intern_intro_pattern lf ist ids)) | TacDoubleInduction (h1,h2) -> let h1 = intern_quantified_hypothesis ist h1 in @@ -738,14 +738,14 @@ let rec intern_atomic lf ist x = | TacLeft bl -> TacLeft (intern_bindings ist bl) | TacRight bl -> TacRight (intern_bindings ist bl) | TacSplit (b,bl) -> TacSplit (b,intern_bindings ist bl) - | TacAnyConstructor t -> TacAnyConstructor (option_map (intern_tactic ist) t) + | TacAnyConstructor t -> TacAnyConstructor (Option.map (intern_tactic ist) t) | TacConstructor (n,bl) -> TacConstructor (n, intern_bindings ist bl) (* Conversion *) | TacReduce (r,cl) -> TacReduce (intern_red_expr ist r, clause_app (intern_hyp_location ist) cl) | TacChange (occl,c,cl) -> - TacChange (option_map (intern_constr_occurrence ist) occl, + TacChange (Option.map (intern_constr_occurrence ist) occl, (if occl = None then intern_type ist c else intern_constr ist c), clause_app (intern_hyp_location ist) cl) @@ -791,7 +791,7 @@ and intern_tactic_seq ist = function | TacLetIn (l,u) -> let l = List.map (fun (n,c,b) -> - (n,option_map (intern_tactic ist) c, intern_tacarg !strict_check ist b)) l in + (n,Option.map (intern_tactic ist) c, intern_tacarg !strict_check ist b)) l in let (l1,l2) = ist.ltacvars in let ist' = { ist with ltacvars = ((extract_let_names l)@l1,l2) } in ist.ltacvars, TacLetIn (l,intern_tactic ist' u) @@ -1248,7 +1248,7 @@ let interp_hyp_location ist gl ((occs,id),hl) = ((interp_int_or_var_list ist occs,interp_hyp ist gl id),hl) let interp_clause ist gl { onhyps=ol; onconcl=b; concl_occs=occs } = - { onhyps=option_map(List.map (interp_hyp_location ist gl)) ol; + { onhyps=Option.map(List.map (interp_hyp_location ist gl)) ol; onconcl=b; concl_occs= interp_int_or_var_list ist occs } @@ -1440,7 +1440,7 @@ let interp_red_expr ist sigma env = function | Cbv f -> Cbv (interp_flag ist env f) | Lazy f -> Lazy (interp_flag ist env f) | Pattern l -> Pattern (List.map (interp_pattern ist sigma env) l) - | Simpl o -> Simpl (option_map (interp_pattern ist sigma env) o) + | Simpl o -> Simpl (Option.map (interp_pattern ist sigma env) o) | (Red _ | Hnf | ExtraRedExpr _ | CbvVm as r) -> r let pf_interp_red_expr ist gl = interp_red_expr ist (project gl) (pf_env gl) @@ -2037,8 +2037,8 @@ and interp_atomic ist gl = function | TacIntrosUntil hyp -> h_intros_until (interp_quantified_hypothesis ist hyp) | TacIntroMove (ido,ido') -> - h_intro_move (option_map (interp_fresh_ident ist gl) ido) - (option_map (interp_hyp ist gl) ido') + h_intro_move (Option.map (interp_fresh_ident ist gl) ido) + (Option.map (interp_hyp ist gl) ido') | TacAssumption -> h_assumption | TacExact c -> h_exact (pf_interp_casted_constr ist gl c) | TacExactNoCheck c -> h_exact_no_check (pf_interp_constr ist gl c) @@ -2046,15 +2046,15 @@ and interp_atomic ist gl = function | TacApply (ev,cb) -> h_apply ev (interp_constr_with_bindings ist gl cb) | TacElim (ev,cb,cbo) -> h_elim ev (interp_constr_with_bindings ist gl cb) - (option_map (interp_constr_with_bindings ist gl) cbo) + (Option.map (interp_constr_with_bindings ist gl) cbo) | TacElimType c -> h_elim_type (pf_interp_type ist gl c) | TacCase (ev,cb) -> h_case ev (interp_constr_with_bindings ist gl cb) | TacCaseType c -> h_case_type (pf_interp_type ist gl c) - | TacFix (idopt,n) -> h_fix (option_map (interp_fresh_ident ist gl) idopt) n + | TacFix (idopt,n) -> h_fix (Option.map (interp_fresh_ident ist gl) idopt) n | TacMutualFix (id,n,l) -> let f (id,n,c) = (interp_fresh_ident ist gl id,n,pf_interp_type ist gl c) in h_mutual_fix (interp_fresh_ident ist gl id) n (List.map f l) - | TacCofix idopt -> h_cofix (option_map (interp_fresh_ident ist gl) idopt) + | TacCofix idopt -> h_cofix (Option.map (interp_fresh_ident ist gl) idopt) | TacMutualCofix (id,l) -> let f (id,c) = (interp_fresh_ident ist gl id,pf_interp_type ist gl c) in h_mutual_cofix (interp_fresh_ident ist gl id) (List.map f l) @@ -2062,7 +2062,7 @@ and interp_atomic ist gl = function | TacAssert (t,ipat,c) -> let c = (if t=None then pf_interp_constr else pf_interp_type) ist gl c in abstract_tactic (TacAssert (t,ipat,inj_open c)) - (Tactics.forward (option_map (interp_tactic ist) t) + (Tactics.forward (Option.map (interp_tactic ist) t) (interp_intro_pattern ist gl ipat) c) | TacGeneralize cl -> h_generalize (pf_interp_constr_list ist gl cl) | TacGeneralizeDep c -> h_generalize_dep (pf_interp_constr ist gl c) @@ -2073,17 +2073,17 @@ and interp_atomic ist gl = function (* Automation tactics *) | TacTrivial (lems,l) -> Auto.h_trivial (pf_interp_constr_list ist gl lems) - (option_map (List.map (interp_hint_base ist)) l) + (Option.map (List.map (interp_hint_base ist)) l) | TacAuto (n,lems,l) -> - Auto.h_auto (option_map (interp_int_or_var ist) n) + Auto.h_auto (Option.map (interp_int_or_var ist) n) (pf_interp_constr_list ist gl lems) - (option_map (List.map (interp_hint_base ist)) l) + (Option.map (List.map (interp_hint_base ist)) l) | TacAutoTDB n -> Dhyp.h_auto_tdb n | TacDestructHyp (b,id) -> Dhyp.h_destructHyp b (interp_hyp ist gl id) | TacDestructConcl -> Dhyp.h_destructConcl | TacSuperAuto (n,l,b1,b2) -> Auto.h_superauto n l b1 b2 | TacDAuto (n,p,lems) -> - Auto.h_dauto (option_map (interp_int_or_var ist) n,p) + Auto.h_dauto (Option.map (interp_int_or_var ist) n,p) (pf_interp_constr_list ist gl lems) (* Derived basic tactics *) @@ -2091,13 +2091,13 @@ and interp_atomic ist gl = function h_simple_induction (interp_quantified_hypothesis ist h) | TacNewInduction (ev,lc,cbo,ids) -> h_new_induction ev (List.map (interp_induction_arg ist gl) lc) - (option_map (interp_constr_with_bindings ist gl) cbo) + (Option.map (interp_constr_with_bindings ist gl) cbo) (interp_intro_pattern ist gl ids) | TacSimpleDestruct h -> h_simple_destruct (interp_quantified_hypothesis ist h) | TacNewDestruct (ev,c,cbo,ids) -> h_new_destruct ev (List.map (interp_induction_arg ist gl) c) - (option_map (interp_constr_with_bindings ist gl) cbo) + (Option.map (interp_constr_with_bindings ist gl) cbo) (interp_intro_pattern ist gl ids) | TacDoubleInduction (h1,h2) -> let h1 = interp_quantified_hypothesis ist h1 in @@ -2128,7 +2128,7 @@ and interp_atomic ist gl = function | TacSplit (_,bl) -> h_split (interp_bindings ist gl bl) | TacAnyConstructor t -> abstract_tactic (TacAnyConstructor t) - (Tactics.any_constructor (option_map (interp_tactic ist) t)) + (Tactics.any_constructor (Option.map (interp_tactic ist) t)) | TacConstructor (n,bl) -> h_constructor (skip_metaid n) (interp_bindings ist gl bl) @@ -2136,7 +2136,7 @@ and interp_atomic ist gl = function | TacReduce (r,cl) -> h_reduce (pf_interp_red_expr ist gl r) (interp_clause ist gl cl) | TacChange (occl,c,cl) -> - h_change (option_map (pf_interp_pattern ist gl) occl) + h_change (Option.map (pf_interp_pattern ist gl) occl) (if occl = None then pf_interp_type ist gl c else pf_interp_constr ist gl c) (interp_clause ist gl cl) @@ -2152,7 +2152,7 @@ and interp_atomic ist gl = function (List.map (fun (b,c) -> (b, interp_constr_with_bindings ist gl c)) l) (interp_clause ist gl cl) | TacInversion (DepInversion (k,c,ids),hyp) -> - Inv.dinv k (option_map (pf_interp_constr ist gl) c) + Inv.dinv k (Option.map (pf_interp_constr ist gl) c) (interp_intro_pattern ist gl ids) (interp_declared_or_quantified_hypothesis ist gl hyp) | TacInversion (NonDepInversion (k,idl,ids),hyp) -> @@ -2201,7 +2201,7 @@ and interp_atomic ist gl = function | ExtraArgType s when tactic_genarg_level s <> None -> (* Special treatment of tactic arguments *) val_interp ist gl - (out_gen (globwit_tactic (out_some (tactic_genarg_level s))) x) + (out_gen (globwit_tactic (Option.get (tactic_genarg_level s))) x) | List0ArgType ConstrArgType -> let wit = wit_list0 globwit_constr in VList (List.map (mk_constr_value ist gl) (out_gen wit x)) @@ -2348,7 +2348,7 @@ let subst_redexp subst = function | Cbv f -> Cbv (subst_flag subst f) | Lazy f -> Lazy (subst_flag subst f) | Pattern l -> Pattern (List.map (subst_constr_occurrence subst) l) - | Simpl o -> Simpl (option_map (subst_constr_occurrence subst) o) + | Simpl o -> Simpl (Option.map (subst_constr_occurrence subst) o) | (Red _ | Hnf | ExtraRedExpr _ | CbvVm as r) -> r let subst_raw_may_eval subst = function @@ -2377,7 +2377,7 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with | TacApply (ev,cb) -> TacApply (ev,subst_raw_with_bindings subst cb) | TacElim (ev,cb,cbo) -> TacElim (ev,subst_raw_with_bindings subst cb, - option_map (subst_raw_with_bindings subst) cbo) + Option.map (subst_raw_with_bindings subst) cbo) | TacElimType c -> TacElimType (subst_rawconstr subst c) | TacCase (ev,cb) -> TacCase (ev,subst_raw_with_bindings subst cb) | TacCaseType c -> TacCaseType (subst_rawconstr subst c) @@ -2389,7 +2389,7 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with TacMutualCofix (id, List.map (fun (id,c) -> (id,subst_rawconstr subst c)) l) | TacCut c -> TacCut (subst_rawconstr subst c) | TacAssert (b,na,c) -> - TacAssert (option_map (subst_tactic subst) b,na,subst_rawconstr subst c) + TacAssert (Option.map (subst_tactic subst) b,na,subst_rawconstr subst c) | TacGeneralize cl -> TacGeneralize (List.map (subst_rawconstr subst) cl) | TacGeneralizeDep c -> TacGeneralizeDep (subst_rawconstr subst c) | TacLetTac (id,c,clp) -> TacLetTac (id,subst_rawconstr subst c,clp) @@ -2407,11 +2407,11 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with | TacSimpleInduction h as x -> x | TacNewInduction (ev,lc,cbo,ids) -> TacNewInduction (ev,List.map (subst_induction_arg subst) lc, - option_map (subst_raw_with_bindings subst) cbo, ids) + Option.map (subst_raw_with_bindings subst) cbo, ids) | TacSimpleDestruct h as x -> x | TacNewDestruct (ev,c,cbo,ids) -> TacNewDestruct (ev,List.map (subst_induction_arg subst) c, - option_map (subst_raw_with_bindings subst) cbo, ids) + Option.map (subst_raw_with_bindings subst) cbo, ids) | TacDoubleInduction (h1,h2) as x -> x | TacDecomposeAnd c -> TacDecomposeAnd (subst_rawconstr subst c) | TacDecomposeOr c -> TacDecomposeOr (subst_rawconstr subst c) @@ -2431,13 +2431,13 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with | TacLeft bl -> TacLeft (subst_bindings subst bl) | TacRight bl -> TacRight (subst_bindings subst bl) | TacSplit (b,bl) -> TacSplit (b,subst_bindings subst bl) - | TacAnyConstructor t -> TacAnyConstructor (option_map (subst_tactic subst) t) + | TacAnyConstructor t -> TacAnyConstructor (Option.map (subst_tactic subst) t) | TacConstructor (n,bl) -> TacConstructor (n, subst_bindings subst bl) (* Conversion *) | TacReduce (r,cl) -> TacReduce (subst_redexp subst r, cl) | TacChange (occl,c,cl) -> - TacChange (option_map (subst_constr_occurrence subst) occl, + TacChange (Option.map (subst_constr_occurrence subst) occl, subst_rawconstr subst c, cl) (* Equivalence relations *) @@ -2450,7 +2450,7 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with List.map (fun (b,c) ->b,subst_raw_with_bindings subst c) l, cl) | TacInversion (DepInversion (k,c,l),hyp) -> - TacInversion (DepInversion (k,option_map (subst_rawconstr subst) c,l),hyp) + TacInversion (DepInversion (k,Option.map (subst_rawconstr subst) c,l),hyp) | TacInversion (NonDepInversion _,_) as x -> x | TacInversion (InversionUsing (c,cl),hyp) -> TacInversion (InversionUsing (subst_rawconstr subst c,cl),hyp) @@ -2469,7 +2469,7 @@ and subst_tactic subst (t:glob_tactic_expr) = match t with let lrc = List.map (fun (n,b) -> (n,subst_tactic_fun subst b)) lrc in TacLetRecIn (lrc,(subst_tactic subst u:glob_tactic_expr)) | TacLetIn (l,u) -> - let l = List.map (fun (n,c,b) -> (n,option_map (subst_tactic subst) c,subst_tacarg subst b)) l in + let l = List.map (fun (n,c,b) -> (n,Option.map (subst_tactic subst) c,subst_tacarg subst b)) l in TacLetIn (l,subst_tactic subst u) | TacMatchContext (lz,lr,lmr) -> TacMatchContext(lz,lr, subst_match_rule subst lmr) diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 3121d3a49..782f2a4c1 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -60,7 +60,7 @@ let inj_open c = (Evd.empty,c) let inj_occ (occ,c) = (occ,inj_open c) let inj_red_expr = function - | Simpl lo -> Simpl (option_map inj_occ lo) + | Simpl lo -> Simpl (Option.map inj_occ lo) | Fold l -> Fold (List.map inj_open l) | Pattern l -> Pattern (List.map inj_occ l) | (ExtraRedExpr _ | CbvVm | Red _ | Hnf | Cbv _ | Lazy _ | Unfold _ as c) @@ -1694,7 +1694,7 @@ let mkHRefl t x = [| t; x |]) let mkCoe a x p px y eq = - mkApp (out_some (build_coq_eq_data ()).rect, [| a; x; p; px; y; eq |]) + mkApp (Option.get (build_coq_eq_data ()).rect, [| a; x; p; px; y; eq |]) let lift_togethern n l = let l', _ = diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 933b23c53..7546ad310 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -321,7 +321,7 @@ let init is_ide = set_vm_opt (); engage (); if (not !batch_mode|| !compile_list=[]) && Global.env_is_empty() then - option_iter Declaremods.start_library !toplevel_name; + Option.iter Declaremods.start_library !toplevel_name; init_library_roots (); load_vernac_obj (); require (); diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml index e25ff99e0..bb30c669f 100644 --- a/toplevel/himsg.ml +++ b/toplevel/himsg.ml @@ -320,7 +320,7 @@ let explain_hole_kind env = function | BinderType Anonymous -> str "the type of this anonymous binder" | ImplicitArg (c,(n,ido)) -> - let id = out_some ido in + let id = Option.get ido in str "the implicit parameter " ++ pr_id id ++ spc () ++ str "of" ++ spc () ++ Nametab.pr_global_env Idset.empty c diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml index 9a162997b..7ebf3dfa9 100644 --- a/toplevel/metasyntax.ml +++ b/toplevel/metasyntax.ml @@ -763,21 +763,21 @@ let find_precedence lev etyps symbols = | ETPattern | ETOther _ -> (* Give a default ? *) if lev = None then error "Need an explicit level" - else out_some lev + else Option.get lev | ETConstrList _ -> assert false (* internally used in grammar only *) with Not_found -> if lev = None then error "A left-recursive notation must have an explicit level" - else out_some lev) + else Option.get lev) | Terminal _ ::l when (match list_last symbols with Terminal _ -> true |_ -> false) -> if lev = None then (Options.if_verbose msgnl (str "Setting notation at level 0"); 0) - else out_some lev + else Option.get lev | _ -> if lev = None then error "Cannot determine the level"; - out_some lev + Option.get lev let check_curly_brackets_notation_exists () = try let _ = Notation.level_of_notation "{ _ }" in () @@ -839,7 +839,7 @@ let compute_syntax_data (df,modifiers) = (* Registration of notations interpretation *) let load_notation _ (_,(_,scope,pat,onlyparse,_)) = - option_iter Notation.declare_scope scope + Option.iter Notation.declare_scope scope let open_notation i (_,(_,scope,pat,onlyparse,(ntn,df))) = if i=1 & not (Notation.exists_notation_in_scope scope ntn pat) then begin diff --git a/toplevel/minicoq.ml b/toplevel/minicoq.ml index 19fd343e5..e22b33e24 100644 --- a/toplevel/minicoq.ml +++ b/toplevel/minicoq.ml @@ -54,7 +54,7 @@ let check c = let definition id ty c = let c = globalize [] c in - let ty = option_map (globalize []) ty in + let ty = Option.map (globalize []) ty in let ce = { const_entry_body = c; const_entry_type = ty } in let sp = make_path [] id CCI in env := add_constant sp ce (locals()) !env; diff --git a/toplevel/toplevel.ml b/toplevel/toplevel.ml index fbdc96d6e..aba5aeb27 100644 --- a/toplevel/toplevel.ml +++ b/toplevel/toplevel.ml @@ -103,7 +103,7 @@ let get_bols_of_loc ibuf (bp,ep) = lines_rec ll nafter fl in let (fl,ll) = lines_rec ibuf.len ([],None) ibuf.bols in - (fl,out_some ll) + (fl,Option.get ll) let dotted_location (b,e) = if e-b < 3 then diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index d6b874c22..9cb2b26b7 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -298,7 +298,7 @@ let vernac_notation = Metasyntax.add_notation let start_proof_and_print idopt k t hook = start_proof_com idopt k t hook; print_subgoals (); - if !pcoq <> None then (out_some !pcoq).start_proof () + if !pcoq <> None then (Option.get !pcoq).start_proof () let vernac_definition (local,_,_ as k) id def hook = match def with @@ -386,7 +386,7 @@ let vernac_declare_module export id binders_ast mty_ast_o = Modintern.interp_modtype Modintern.interp_modexpr id binders_ast (Some mty_ast_o) None; if_verbose message ("Module "^ string_of_id id ^" is declared"); - option_iter (fun export -> vernac_import export [Ident (dummy_loc,id)]) export + Option.iter (fun export -> vernac_import export [Ident (dummy_loc,id)]) export let vernac_define_module export id binders_ast mty_ast_o mexpr_ast_o = (* We check the state of the system (in section, in module type) @@ -406,7 +406,7 @@ let vernac_define_module export id binders_ast mty_ast_o mexpr_ast_o = ("Interactive Module "^ string_of_id id ^" started") ; List.iter (fun (export,id) -> - option_iter + Option.iter (fun export -> vernac_import export [Ident (dummy_loc,id)]) export ) argsexport | Some _ -> @@ -422,13 +422,13 @@ let vernac_define_module export id binders_ast mty_ast_o mexpr_ast_o = id binders_ast mty_ast_o mexpr_ast_o; if_verbose message ("Module "^ string_of_id id ^" is defined"); - option_iter (fun export -> vernac_import export [Ident (dummy_loc,id)]) + Option.iter (fun export -> vernac_import export [Ident (dummy_loc,id)]) export let vernac_end_module export id = Declaremods.end_module id; if_verbose message ("Module "^ string_of_id id ^" is defined") ; - option_iter (fun export -> vernac_import export [Ident (dummy_loc,id)]) export + Option.iter (fun export -> vernac_import export [Ident (dummy_loc,id)]) export let vernac_declare_module_type id binders_ast mty_ast_o = @@ -447,7 +447,7 @@ let vernac_declare_module_type id binders_ast mty_ast_o = ("Interactive Module Type "^ string_of_id id ^" started"); List.iter (fun (export,id) -> - option_iter + Option.iter (fun export -> vernac_import export [Ident (dummy_loc,id)]) export ) argsexport @@ -542,7 +542,7 @@ let vernac_solve n tcom b = reset_top_of_script () end; print_subgoals(); - if !pcoq <> None then (out_some !pcoq).solve n + if !pcoq <> None then (Option.get !pcoq).solve n (* A command which should be a tactic. It has been added by Christine to patch an error in the design of the proof @@ -910,12 +910,12 @@ let vernac_check_may_eval redexp glopt rc = let j = Typeops.typing env c in match redexp with | None -> - if !pcoq <> None then (out_some !pcoq).print_check env j + if !pcoq <> None then (Option.get !pcoq).print_check env j else msg (print_judgment env j) | Some r -> let redfun = fst (reduction_of_red_expr (interp_redexp env evmap r)) in if !pcoq <> None - then (out_some !pcoq).print_eval redfun env evmap rc j + then (Option.get !pcoq).print_eval redfun env evmap rc j else msg (print_eval redfun env evmap rc j) (* The same but avoiding the current goal context if any *) @@ -940,7 +940,7 @@ let vernac_print = function | PrintMLLoadPath -> Mltop.print_ml_path () | PrintMLModules -> Mltop.print_ml_modules () | PrintName qid -> - if !pcoq <> None then (out_some !pcoq).print_name qid + if !pcoq <> None then (Option.get !pcoq).print_name qid else msg (print_name qid) | PrintOpaqueName qid -> msg (print_opaque_name qid) | PrintGraph -> ppnl (Prettyp.print_graph()) @@ -995,7 +995,7 @@ let interp_search_about_item = function let vernac_search s r = let r = interp_search_restriction r in - if !pcoq <> None then (out_some !pcoq).search s r else + if !pcoq <> None then (Option.get !pcoq).search s r else match s with | SearchPattern c -> let _,pat = interp_constrpattern Evd.empty (Global.env()) c in @@ -1034,12 +1034,12 @@ let vernac_abort = function | None -> delete_current_proof (); if_verbose message "Current goal aborted"; - if !pcoq <> None then (out_some !pcoq).abort "" + if !pcoq <> None then (Option.get !pcoq).abort "" | Some id -> delete_proof id; let s = string_of_id (snd id) in if_verbose message ("Goal "^s^" aborted"); - if !pcoq <> None then (out_some !pcoq).abort s + if !pcoq <> None then (Option.get !pcoq).abort s let vernac_abort_all () = if refining() then begin @@ -1109,7 +1109,7 @@ let explain_tree occ = let vernac_show = function | ShowGoal nopt -> - if !pcoq <> None then (out_some !pcoq).show_goal nopt + if !pcoq <> None then (Option.get !pcoq).show_goal nopt else msg (match nopt with | None -> pr_open_subgoals () | Some n -> pr_nth_open_subgoal n) |