aboutsummaryrefslogtreecommitdiff
path: root/contrib
diff options
context:
space:
mode:
Diffstat (limited to 'contrib')
-rw-r--r--contrib/correctness/pmisc.ml2
-rw-r--r--contrib/correctness/pmonad.ml6
-rw-r--r--contrib/correctness/psyntax.ml42
-rw-r--r--contrib/correctness/putil.ml6
-rw-r--r--contrib/correctness/pwp.ml6
-rw-r--r--contrib/extraction/extract_env.ml16
-rw-r--r--contrib/extraction/extraction.ml4
-rw-r--r--contrib/extraction/modutil.ml10
-rw-r--r--contrib/extraction/ocaml.ml2
-rw-r--r--contrib/first-order/g_ground.ml48
-rw-r--r--contrib/funind/functional_principles_proofs.ml8
-rw-r--r--contrib/funind/functional_principles_types.ml6
-rw-r--r--contrib/funind/indfun.ml14
-rw-r--r--contrib/funind/indfun_common.ml36
-rw-r--r--contrib/funind/invfun.ml18
-rw-r--r--contrib/funind/rawterm_to_relation.ml8
-rw-r--r--contrib/funind/rawtermops.ml24
-rw-r--r--contrib/interface/blast.ml4
-rw-r--r--contrib/interface/xlate.ml16
-rw-r--r--contrib/ring/ring.ml10
-rw-r--r--contrib/setoid_ring/newring.ml42
-rw-r--r--contrib/subtac/subtac_cases.ml24
-rw-r--r--contrib/subtac/subtac_coercion.ml10
-rw-r--r--contrib/subtac/subtac_command.ml4
-rw-r--r--contrib/subtac/subtac_obligations.ml2
-rw-r--r--contrib/subtac/subtac_pretyping_F.ml6
-rw-r--r--contrib/xml/xmlcommand.ml4
27 files changed, 129 insertions, 129 deletions
diff --git a/contrib/correctness/pmisc.ml b/contrib/correctness/pmisc.ml
index 6b14fd3048..23c1028a41 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 1a4ddbc2c7..a341ba2ba3 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 72b609b24d..bb9a355c3f 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 46cd124039..e4bac65f4b 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 70e9eee293..258a461501 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 b6367d98a2..2aca56f9bb 100644
--- a/contrib/extraction/extract_env.ml
+++ b/contrib/extraction/extract_env.ml
@@ -241,7 +241,7 @@ and extract_meb env mpo all = function
and extract_module env mp all mb =
(* [mb.mod_expr <> None ], since we look at modules from outside. *)
(* Example of module with empty [mod_expr] is X inside a Module F [X:SIG]. *)
- let meb = out_some mb.mod_expr in
+ let meb = Option.get mb.mod_expr in
let mtb = match mb.mod_user_type with None -> mb.mod_type | Some mt -> mt in
(* Because of the "with" construct, the module type can be [MTBsig] with *)
(* a msid different from the one of the module. Here is the patch. *)
@@ -282,7 +282,7 @@ let mono_filename f =
Filename.chop_suffix f d.file_suffix
else f
in
- Some (f^d.file_suffix), option_map ((^) f) d.sig_suffix, id_of_string f
+ Some (f^d.file_suffix), Option.map ((^) f) d.sig_suffix, id_of_string f
(* Builds a suitable filename from a module id *)
@@ -290,7 +290,7 @@ let module_filename m =
let d = descr () in
let f = if d.capital_file then String.capitalize else String.uncapitalize in
let fn = f (string_of_id m) in
- Some (fn^d.file_suffix), option_map ((^) fn) d.sig_suffix, m
+ Some (fn^d.file_suffix), Option.map ((^) fn) d.sig_suffix, m
(*s Extraction of one decl to stdout. *)
@@ -317,7 +317,7 @@ let print_structure_to_file (fn,si,mo) struc =
else struct_ast_search (function MLmagic _ -> true | _ -> false) struc }
in
(* print the implementation *)
- let cout = option_map open_out fn in
+ let cout = Option.map open_out fn in
let ft = match cout with
| None -> !Pp_control.std_ft
| Some cout -> Pp_control.with_output_to cout in
@@ -330,13 +330,13 @@ let print_structure_to_file (fn,si,mo) struc =
reset_renaming_tables OnlyLocal;
end;
msg_with ft (d.pp_struct struc);
- option_iter close_out cout;
+ Option.iter close_out cout;
with e ->
- option_iter close_out cout; raise e
+ Option.iter close_out cout; raise e
end;
- option_iter info_file fn;
+ Option.iter info_file fn;
(* print the signature *)
- option_iter
+ Option.iter
(fun si ->
let cout = open_out si in
let ft = Pp_control.with_output_to cout in
diff --git a/contrib/extraction/extraction.ml b/contrib/extraction/extraction.ml
index 77067b2b4c..27687ae1c3 100644
--- a/contrib/extraction/extraction.ml
+++ b/contrib/extraction/extraction.ml
@@ -310,7 +310,7 @@ and extract_ind env kn = (* kn is supposed to be in long form *)
with Not_found ->
(* First, if this inductive is aliased via a Module, *)
(* we process the original inductive. *)
- option_iter (fun kn -> ignore (extract_ind env kn)) mib.mind_equiv;
+ Option.iter (fun kn -> ignore (extract_ind env kn)) mib.mind_equiv;
(* Everything concerning parameters. *)
(* We do that first, since they are common to all the [mib]. *)
let mip0 = mib.mind_packets.(0) in
@@ -413,7 +413,7 @@ and extract_ind env kn = (* kn is supposed to be in long form *)
(Inductive.type_of_inductive env (mib,mip0))
in
List.iter
- (option_iter
+ (Option.iter
(fun kn -> if Cset.mem kn !projs then add_projection n kn))
(lookup_projections ip)
with Not_found -> ()
diff --git a/contrib/extraction/modutil.ml b/contrib/extraction/modutil.ml
index 760f76c9a3..79ba0ebc5e 100644
--- a/contrib/extraction/modutil.ml
+++ b/contrib/extraction/modutil.ml
@@ -39,9 +39,9 @@ let add_structure mp msb env =
let rec subst_module sub mb =
let mtb' = Modops.subst_modtype sub mb.mod_type
- and meb' = option_smartmap (subst_meb sub) mb.mod_expr
- and mtb'' = option_smartmap (Modops.subst_modtype sub) mb.mod_user_type
- and mpo' = option_smartmap (subst_mp sub) mb.mod_equiv in
+ and meb' = Option.smartmap (subst_meb sub) mb.mod_expr
+ and mtb'' = Option.smartmap (Modops.subst_modtype sub) mb.mod_user_type
+ and mpo' = Option.smartmap (subst_mp sub) mb.mod_equiv in
if (mtb'==mb.mod_type) && (meb'==mb.mod_expr) &&
(mtb''==mb.mod_user_type) && (mpo'==mb.mod_equiv)
then mb
@@ -170,7 +170,7 @@ let decl_iter_references do_term do_cons do_type =
let spec_iter_references do_term do_cons do_type = function
| Sind (kn,ind) -> ind_iter_references do_term do_cons do_type kn ind
- | Stype (r,_,ot) -> do_type r; option_iter (type_iter_references do_type) ot
+ | Stype (r,_,ot) -> do_type r; Option.iter (type_iter_references do_type) ot
| Sval (r,t) -> do_term r; type_iter_references do_type t
let struct_iter_references do_term do_cons do_type =
@@ -241,7 +241,7 @@ let spec_type_search f = function
| Sind (_,{ind_packets=p}) ->
Array.iter
(fun {ip_types=v} -> Array.iter (List.iter (type_search f)) v) p
- | Stype (_,_,ot) -> option_iter (type_search f) ot
+ | Stype (_,_,ot) -> Option.iter (type_search f) ot
| Sval (_,u) -> type_search f u
let struct_type_search f s =
diff --git a/contrib/extraction/ocaml.ml b/contrib/extraction/ocaml.ml
index f3df9230d0..8ba07ab0b7 100644
--- a/contrib/extraction/ocaml.ml
+++ b/contrib/extraction/ocaml.ml
@@ -574,7 +574,7 @@ and pp_module_type ol = function
str "functor (" ++ name ++ str ":" ++ typ ++ str ") ->" ++ fnl () ++ def
| MTsig (msid, sign) ->
let tvm = top_visible_mp () in
- option_iter (fun l -> add_subst msid (MPdot (tvm, l))) ol;
+ Option.iter (fun l -> add_subst msid (MPdot (tvm, l))) ol;
let mp = MPself msid in
push_visible mp;
let l = map_succeed pp_specif sign in
diff --git a/contrib/first-order/g_ground.ml4 b/contrib/first-order/g_ground.ml4
index e48d47d9db..3ee1db14c9 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 b10aa782c8..45976d6e5b 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 cb804f6f2b..72f930b0a6 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 199e01525b..3102f1b5d7 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 609504ba5a..c2372d3ed0 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 6171e81948..dcbefe4a40 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 b34a1097a3..af0a2addc8 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 f9e188dacf..e8cce47adb 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 207d78b193..82fbe9c691 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 150b070f88..0e4f660724 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 e81c9ddd5c..97dd2f143a 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 1cbae1e2ff..2c6e0ebcd4 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 e54c59058f..34c398289a 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 1fb079fac6..17bbb65bdc 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 d7d304279a..49eab5d29d 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 769aff9dcf..5e7f025be1 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 ab542feb20..0ed0632c65 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 1aabd4348e..82d7c19e51 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 ^ "\"")
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-19 13:34:15 +0000