diff options
| author |  aspiwack <aspiwack@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-12-05 21:11:19 +0000 |
|---|---|---|
| committer | aspiwack <aspiwack@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-12-05 21:11:19 +0000 |
| commit | fb75bd254df2eadfc8abd45a646dfe9b1c4a53b6 (patch) | |
| tree | 4e1e289a56b97ec2a8fe9de2ac0e6418f7c48d2b | |
| parent | c6d34ae80622b409733776c3cc4ecf5fce6a8378 (diff) | |
Factorisation des opérations sur le type option de Util dans un module
lib/option.ml(i) . J'en profite pour rajouter des primitives de lifting
des fonctions (à un ou deux arguments tous ou partie de type option).
Il reste quelques opérations dans Util à propos desquelles je ne suis
pas trop sûr, ou simplement que j'ai oublié, mais qui attendront demain
car il est tard (comme some_in qui devrait devenir Option.make je
suppose) . Elles s'expriment souvent facilement en fonction des
autres, par exemple "option_compare x y" est égal à "Option.lift2 compare x y"
. Le option_cons devrait faire son chemin dans le module parce qu'il est
assez primitif et qu'il n'y a pas de fonction "cons" dans OCaml.
J'en ai profité aussi pour remplacer les trop nombreux "failwith" par
des erreurs locales au module, donc plus robustes.
J'ai trouvé aussi une fonction qui était définie deux fois, et une
définie dans un module particulier.
Mon seul bémol (mais facile à traiter) c'est la proximité entre le
nom de module Option et l'ancien Options. J'ai pas de meilleure idée de
nom à l'heure qu'il est, ni pour l'un, ni pour l'autre.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10346 85f007b7-540e-0410-9357-904b9bb8a0f7
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) |