aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-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/common.ml2
-rw-r--r--contrib/first-order/g_ground.ml48
-rw-r--r--contrib/funind/rawtermops.ml14
-rw-r--r--contrib/interface/xlate.ml4
-rw-r--r--contrib/subtac/eterm.ml4
-rw-r--r--contrib/subtac/subtac_coercion.ml10
-rw-r--r--contrib/subtac/subtac_command.ml2
-rw-r--r--ide/coqide.ml2
-rw-r--r--interp/constrextern.ml12
-rw-r--r--interp/constrintern.ml6
-rw-r--r--interp/genarg.ml2
-rw-r--r--interp/notation.ml6
-rw-r--r--interp/reserve.ml8
-rw-r--r--interp/topconstr.ml24
-rw-r--r--kernel/cooking.ml2
-rw-r--r--kernel/declarations.ml4
-rw-r--r--kernel/environ.ml2
-rw-r--r--kernel/modops.ml2
-rw-r--r--kernel/safe_typing.ml6
-rw-r--r--kernel/sign.ml2
-rw-r--r--kernel/term.ml2
-rw-r--r--lib/options.ml2
-rw-r--r--lib/util.ml2
-rw-r--r--lib/util.mli2
-rw-r--r--library/declare.ml2
-rw-r--r--library/declaremods.ml2
-rw-r--r--library/lib.ml2
-rw-r--r--library/libobject.ml4
-rw-r--r--parsing/egrammar.ml4
-rw-r--r--parsing/g_ascii_syntax.ml2
-rw-r--r--parsing/g_constr.ml42
-rw-r--r--parsing/g_tactic.ml42
-rw-r--r--parsing/g_vernac.ml42
-rw-r--r--parsing/prettyp.ml2
-rw-r--r--pretyping/cases.ml16
-rw-r--r--pretyping/clenv.ml8
-rw-r--r--pretyping/coercion.ml8
-rw-r--r--pretyping/detyping.ml2
-rw-r--r--pretyping/evarconv.ml2
-rw-r--r--pretyping/evarutil.ml4
-rw-r--r--pretyping/pattern.ml2
-rw-r--r--pretyping/pretype_errors.ml4
-rw-r--r--pretyping/pretyping.ml6
-rw-r--r--pretyping/rawterm.ml10
-rw-r--r--pretyping/recordops.ml2
-rw-r--r--pretyping/tacred.ml2
-rw-r--r--pretyping/termops.ml2
-rw-r--r--tactics/auto.ml2
-rw-r--r--tactics/eauto.ml42
-rw-r--r--tactics/extratactics.ml42
-rw-r--r--tactics/hiddentac.ml2
-rw-r--r--tactics/nbtermdn.ml6
-rw-r--r--tactics/setoid_replace.ml22
-rw-r--r--tactics/tacinterp.ml80
-rw-r--r--toplevel/minicoq.ml2
60 files changed, 181 insertions, 181 deletions
diff --git a/contrib/correctness/pmisc.ml b/contrib/correctness/pmisc.ml
index 403ab8b9d..6b14fd304 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_app (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 5d1e55e3c..1a4ddbc2c 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_app (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_app (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_app (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 ece466849..f6aad378d 100644
--- a/contrib/correctness/psyntax.ml4
+++ b/contrib/correctness/psyntax.ml4
@@ -786,7 +786,7 @@ END
VERNAC COMMAND EXTEND Correctness
[ "Correctness" preident(str) program(pgm) then_tac(tac) ]
- -> [ Ptactic.correctness str pgm (option_app 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 29064578f..46cd12403 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_app (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_app (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_app (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 b7c6ac8c1..70e9eee29 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_app (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_app (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_app (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/common.ml b/contrib/extraction/common.ml
index 2b713c514..1d1383f60 100644
--- a/contrib/extraction/common.ml
+++ b/contrib/extraction/common.ml
@@ -401,7 +401,7 @@ let print_structure_to_file f prm struc =
else struct_ast_search (function MLmagic _ -> true | _ -> false) struc
in
(* print the implementation *)
- let cout = option_app (fun (f,_) -> open_out f) f in
+ let cout = option_map (fun (f,_) -> open_out f) f in
let ft = match cout with
| None -> !Pp_control.std_ft
| Some cout -> Pp_control.with_output_to cout in
diff --git a/contrib/first-order/g_ground.ml4 b/contrib/first-order/g_ground.ml4
index e6f7b03cb..451ac33d8 100644
--- a/contrib/first-order/g_ground.ml4
+++ b/contrib/first-order/g_ground.ml4
@@ -83,14 +83,14 @@ let normalize_evaluables=
TACTIC EXTEND firstorder
[ "firstorder" tactic_opt(t) "with" ne_reference_list(l) ] ->
- [ gen_ground_tac true (option_app eval_tactic t) (Ids l) ]
+ [ gen_ground_tac true (option_map eval_tactic t) (Ids l) ]
| [ "firstorder" tactic_opt(t) "using" ne_preident_list(l) ] ->
- [ gen_ground_tac true (option_app 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_app 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_app eval_tactic t) Void ]
+ [ gen_ground_tac false (option_map eval_tactic t) Void ]
END
diff --git a/contrib/funind/rawtermops.ml b/contrib/funind/rawtermops.ml
index cd09fb5f2..f99aa86c8 100644
--- a/contrib/funind/rawtermops.ml
+++ b/contrib/funind/rawtermops.ml
@@ -113,7 +113,7 @@ let change_vars =
| RLetTuple(loc,nal,(na,rto),b,e) ->
RLetTuple(loc,
nal,
- (na, option_app (change_vars mapping) rto),
+ (na, option_map (change_vars mapping) rto),
change_vars mapping b,
change_vars mapping e
)
@@ -126,7 +126,7 @@ let change_vars =
| RIf(loc,b,(na,e_option),lhs,rhs) ->
RIf(loc,
change_vars mapping b,
- (na,option_app (change_vars mapping) e_option),
+ (na,option_map (change_vars mapping) e_option),
change_vars mapping lhs,
change_vars mapping rhs
)
@@ -292,11 +292,11 @@ let rec alpha_rt excluded rt =
if idmap_is_empty mapping
then rto,t,b
else let replace = change_vars mapping in
- (option_app replace rto,replace t,replace b)
+ (option_map replace rto,replace 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_app (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 =
@@ -305,7 +305,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_app (alpha_rt excluded) e_o),
+ (na,option_map (alpha_rt excluded) e_o),
alpha_rt excluded lhs,
alpha_rt excluded rhs
)
@@ -450,7 +450,7 @@ let replace_var_by_term x_id term =
| RLetTuple(loc,nal,(na,rto),def,b) ->
RLetTuple(loc,
nal,
- (na,option_app replace_var_by_pattern rto),
+ (na,option_map replace_var_by_pattern rto),
replace_var_by_pattern def,
replace_var_by_pattern b
)
@@ -462,7 +462,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_app 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
)
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index a78c35d1d..21138c85e 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -1818,7 +1818,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_app 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
@@ -1860,7 +1860,7 @@ let rec xlate_vernac =
(_, (add_coercion, (_,s)), binders, c1,
rec_constructor_or_none, field_list) ->
let record_constructor =
- xlate_ident_opt (option_app 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)),
diff --git a/contrib/subtac/eterm.ml b/contrib/subtac/eterm.ml
index 5703c0efc..437acb1f2 100644
--- a/contrib/subtac/eterm.ml
+++ b/contrib/subtac/eterm.ml
@@ -128,7 +128,7 @@ let eterm_term evm t tycon =
let anon_evar_bl = List.map (fun (_, x, y) -> (Anonymous, x, y)) evar_bl in
(* Generalize over the existential variables *)
let t'' = Termops.it_mkLambda_or_LetIn t' evar_bl
- and tycon = option_app
+ and tycon = option_map
(fun typ -> Termops.it_mkProd_wo_LetIn typ anon_evar_bl) tycon
in
let _declare_evar (id, c) =
@@ -144,7 +144,7 @@ let eterm_term evm t tycon =
Termops.print_constr_env (Global.env ()) t);
trace (str "Term constructed in eterm" ++ spc () ++
Termops.print_constr_env (Global.env ()) t'');
- ignore(option_app
+ ignore(option_map
(fun typ ->
trace (str "Type :" ++ spc () ++
Termops.print_constr_env (Global.env ()) typ))
diff --git a/contrib/subtac/subtac_coercion.ml b/contrib/subtac/subtac_coercion.ml
index a138c6941..4a9cf8eb4 100644
--- a/contrib/subtac/subtac_coercion.ml
+++ b/contrib/subtac/subtac_coercion.ml
@@ -244,7 +244,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_app (app_opt coercion) v, t
+ !evars, option_map (app_opt coercion) v, t
(* Taken from pretyping/coercion.ml *)
@@ -371,7 +371,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_app (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' ->
@@ -387,7 +387,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_app (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 *)
@@ -404,7 +404,7 @@ module Coercion = struct
let (evd'', v2', t2') =
let v2 =
match v with
- Some v -> option_app (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
@@ -415,7 +415,7 @@ module Coercion = struct
in
inh_conv_coerce_to_fail loc env1 evd' v2 t2 u2
in
- (evd'', option_app (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 727ba82ae..24edeba69 100644
--- a/contrib/subtac/subtac_command.ml
+++ b/contrib/subtac/subtac_command.ml
@@ -209,7 +209,7 @@ let build_recursive (lnameargsardef:(fixpoint_expr * decl_notation) list) boxed
let env', binders_rel = interp_context isevars env0 bl in
let after, ((argname, _, argtyp) as arg), before = list_chop_hd n binders_rel in
let argid = match argname with Name n -> n | _ -> assert(false) in
- let after' = List.map (fun (n, c, t) -> (n, option_app (lift 1) c, lift 1 t)) after in
+ let after' = List.map (fun (n, c, t) -> (n, option_map (lift 1) c, lift 1 t)) after in
let envwf = push_rel_context before env0 in
let wf_rel = interp_constr isevars envwf r in
let accarg_id = id_of_string ("Acc_" ^ string_of_id argid) in
diff --git a/ide/coqide.ml b/ide/coqide.ml
index b4e3b915f..a90f473c1 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -948,7 +948,7 @@ object(self)
self#insert_message s;
message_view#misc#draw None;
if localize then
- (match Util.option_app Util.unloc loc with
+ (match Util.option_map Util.unloc loc with
| None -> ()
| Some (start,stop) ->
let convert_pos = byte_offset_to_char_offset phrase in
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 5efa68e2d..4fbeff526 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -680,7 +680,7 @@ 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_app (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
@@ -690,7 +690,7 @@ let rec extern inctx scopes vars r =
| Name id, RVar (_,id') when id=id' -> None
| Name _, _ -> Some na in
(sub_extern false scopes vars tm,
- (na',option_app (fun (loc,ind,nal) ->
+ (na',option_map (fun (loc,ind,nal) ->
let args = List.map (function
| Anonymous -> RHole (dummy_loc,Evd.InternalHole)
| Name id -> RVar (dummy_loc,id)) nal in
@@ -701,15 +701,15 @@ let rec extern inctx scopes vars r =
| RLetTuple (loc,nal,(na,typopt),tm,b) ->
CLetTuple (loc,nal,
- (option_app (fun _ -> na) typopt,
- option_app (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_app (fun _ -> na) typopt,
- option_app (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) ->
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index aa2c91b20..376360046 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -879,21 +879,21 @@ let internalise sigma globalenv env allow_soapp 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_app (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_app (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_app (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)
diff --git a/interp/genarg.ml b/interp/genarg.ml
index 385171fe3..2c38b4c79 100644
--- a/interp/genarg.ml
+++ b/interp/genarg.ml
@@ -220,7 +220,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_app (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 d068cf64c..74263b768 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -234,12 +234,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_app 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_app 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 ()
@@ -389,7 +389,7 @@ let uninterp_prim_token_cases_pattern c =
let availability_of_prim_token printer_scope scopes =
let f scope = Hashtbl.mem prim_token_interpreter_tab scope in
- option_app snd (find_without_delimiters f (Some printer_scope,None) scopes)
+ option_map snd (find_without_delimiters f (Some printer_scope,None) scopes)
(* Miscellaneous *)
diff --git a/interp/reserve.ml b/interp/reserve.ml
index 834587f8d..85f188599 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_app 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_app 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_app 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_app 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 d82c04e07..cc84d0c10 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -86,14 +86,14 @@ let rawconstr_of_aconstr_with_binders loc g f e = function
let eqnl' = List.map (fun (idl,pat,rhs) ->
let (idl,e) = List.fold_right fold idl ([],e) in
(loc,idl,pat,f e rhs)) eqnl in
- RCases (loc,option_app (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_app g) e nal in
let e,na = name_app g e na in
- RLetTuple (loc,nal,(na,option_app (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_app g e na in
- RIf (loc,f e c,(na,option_app (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,t) -> RCast (loc,f e c,k,f e t)
| ASort x -> RSort (loc,x)
| AHole x -> RHole (loc,x)
@@ -182,20 +182,20 @@ let aconstr_and_vars_of_rawconstr a =
let f (_,idl,pat,rhs) =
found := idl@(!found);
(idl,pat,aux rhs) in
- ACases (option_app aux rtntypopt,
+ ACases (option_map aux rtntypopt,
List.map (fun (tm,(na,x)) ->
add_name found na;
option_iter
(fun (_,_,nl) -> List.iter (add_name found) nl) x;
- (aux tm,(na,option_app (fun (_,ind,nal) -> (ind,nal)) x))) tml,
+ (aux tm,(na,option_map (fun (_,ind,nal) -> (ind,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_app 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_app aux po),aux b1,aux b2)
+ AIf (aux c,(na,option_map aux po),aux b1,aux b2)
| RCast (_,c,k,t) -> ACast (aux c,k,aux t)
| RSort (_,s) -> ASort s
| RHole (_,w) -> AHole w
@@ -289,7 +289,7 @@ let rec subst_aconstr subst bound raw =
and rl' = list_smartmap
(fun (a,(n,signopt) as x) ->
let a' = subst_aconstr subst bound a in
- let signopt' = option_app (fun ((indkn,i),nal as z) ->
+ let signopt' = option_map (fun ((indkn,i),nal as z) ->
let indkn' = subst_kn subst indkn in
if indkn == indkn' then z else ((indkn',i),nal)) signopt in
if a' == a && signopt' == signopt then x else (a',(n,signopt')))
@@ -341,7 +341,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_app (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
@@ -718,15 +718,15 @@ let map_constr_expr_with_binders f g e = function
indnal (option_fold_right (name_fold g) na e))
a e
in
- CCases (loc,option_app (f e') rtnpo,
+ CCases (loc,option_map (f e') rtnpo,
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_app (f e'') po),f e b,f e' c)
+ 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_app (f e') po),f e b1,f e b2)
+ 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 53a9b9644..dffbb76c0 100644
--- a/kernel/cooking.ml
+++ b/kernel/cooking.ml
@@ -113,7 +113,7 @@ type recipe = {
d_modlist : work_list }
let on_body f =
- option_app (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 fbd31f24f..8eb29c4dd 100644
--- a/kernel/declarations.ml
+++ b/kernel/declarations.ml
@@ -171,7 +171,7 @@ type mutual_inductive_body = {
(* 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_app (subst_constr_subst sub) cb.const_body;
+ const_body = option_map (subst_constr_subst sub) cb.const_body;
const_type = type_app (subst_mps 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;*)
@@ -208,7 +208,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_app (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 da41b60e9..a1e41c4ec 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -91,7 +91,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_app 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 166b23007..5fece5b1f 100644
--- a/kernel/modops.ml
+++ b/kernel/modops.ml
@@ -211,7 +211,7 @@ let resolver_of_environment mbid modtype mp env =
if constant.Declarations.const_opaque then
None
else
- option_app Declarations.force
+ option_map Declarations.force
constant.Declarations.const_body
with Not_found -> error_no_such_label (con_label con')
in
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 2a165f74e..38587f7e5 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -245,7 +245,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_app (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 ()
@@ -514,9 +514,9 @@ let import (dp,mb,depends,engmt) digest senv =
let rec lighten_module mb =
{ mb with
- mod_expr = option_app 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_app 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 dd22d5b8c..dbf52498d 100644
--- a/kernel/sign.ml
+++ b/kernel/sign.ml
@@ -89,7 +89,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_app (subst_vars s) b, type_app (subst_vars s) t) in
+ let d = (Name id, option_map (subst_vars s) b, type_app (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 e83c32821..b082c091e 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -643,7 +643,7 @@ let body_of_type ty = ty
type named_declaration = identifier * constr option * types
type rel_declaration = name * constr option * types
-let map_named_declaration f (id, v, ty) = (id, option_app 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
(****************************************************************************)
diff --git a/lib/options.ml b/lib/options.ml
index dab00ac60..b2f2943aa 100644
--- a/lib/options.ml
+++ b/lib/options.ml
@@ -70,11 +70,11 @@ let print_hyps_limit () = !print_hyps_limit
(* A list of the areas of the system where "unsafe" operation
* has been requested *)
+
let unsafe_set = ref Stringset.empty
let add_unsafe s = unsafe_set := Stringset.add s !unsafe_set
let is_unsafe s = Stringset.mem s !unsafe_set
-
(* Dump of globalization (to be used by coqdoc) *)
let dump = ref false
diff --git a/lib/util.ml b/lib/util.ml
index 8b0b1e242..04086e20f 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -682,7 +682,7 @@ let out_some = function
| Some x -> x
| None -> failwith "out_some"
-let option_app f = function
+let option_map f = function
| None -> None
| Some x -> Some (f x)
diff --git a/lib/util.mli b/lib/util.mli
index 1a2fedbdf..ababb2ff9 100644
--- a/lib/util.mli
+++ b/lib/util.mli
@@ -201,7 +201,7 @@ val interval : int -> int -> int list
val in_some : 'a -> 'a option
val out_some : 'a option -> 'a
-val option_app : ('a -> 'b) -> 'a option -> 'b option
+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_left2 : ('a -> 'b -> 'c -> 'a) -> 'a -> 'b option ->
diff --git a/library/declare.ml b/library/declare.ml
index 3835180b1..343bc0c50 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -204,7 +204,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_app 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 39b9fc643..658ca4afb 100644
--- a/library/declaremods.ml
+++ b/library/declaremods.ml
@@ -585,7 +585,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_app (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/lib.ml b/library/lib.ml
index d1bb6599a..bc01c4776 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -460,7 +460,7 @@ let open_section id =
let discharge_item = function
| ((sp,_ as oname),Leaf lobj) ->
- option_app (fun o -> (basename sp,o)) (discharge_object (oname,lobj))
+ option_map (fun o -> (basename sp,o)) (discharge_object (oname,lobj))
| _ ->
None
diff --git a/library/libobject.ml b/library/libobject.ml
index d84e0bc26..b91cbe699 100644
--- a/library/libobject.ml
+++ b/library/libobject.ml
@@ -109,12 +109,12 @@ 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_app 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 exporter lobj =
if Dyn.tag lobj = na then
- option_app 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/parsing/egrammar.ml b/parsing/egrammar.ml
index 336f741ae..f7127ea61 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_app (fun p -> (p,t)) po)
+ | TacNonTerm (_,(nont,t), po) -> (nont, option_map (fun p -> (p,t)) po)
(* Tactic grammar extensions *)
@@ -232,7 +232,7 @@ let make_vprod_item n univ = function
| VTerm s -> (Gramext.Stoken (Lexer.terminal s), None)
| VNonTerm (loc, nt, po) ->
let (etyp, e) = interp_entry_name n univ nt in
- e, option_app (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 e6324e008..ac54fc63d 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_app 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 ed9e1fa06..64d96ae4b 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -75,7 +75,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_app (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 e8829acba..5c847f5a4 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -102,7 +102,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_app (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 0a0df6fb2..94df46be8 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -429,7 +429,7 @@ GEXTEND Gram
(* Implicit *)
| IDENT "Implicit"; IDENT "Arguments"; qid = global;
pos = OPT [ "["; l = LIST0 ident; "]" -> l ] ->
- let pos = option_app (List.map (fun id -> ExplByName id)) pos in
+ let pos = option_map (List.map (fun id -> ExplByName id)) pos in
VernacDeclareImplicits (qid,pos)
| IDENT "Implicit"; ["Type" | IDENT "Types"];
diff --git a/parsing/prettyp.ml b/parsing/prettyp.ml
index 8d99ac112..593595a23 100644
--- a/parsing/prettyp.ml
+++ b/parsing/prettyp.ml
@@ -401,7 +401,7 @@ let print_context with_values =
| h::rest when n = None or out_some n > 0 ->
(match print_library_entry with_values h with
| None -> prec n rest
- | Some pp -> prec (option_app ((+) (-1)) n) rest ++ pp ++ fnl ())
+ | Some pp -> prec (option_map ((+) (-1)) n) rest ++ pp ++ fnl ())
| _ -> mt ()
in
prec
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 57946eacc..425221675 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -429,7 +429,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_app 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
@@ -1167,7 +1167,7 @@ let rec generalize_problem pb current = function
let tomatch = regeneralize_index_tomatch (i+1) tomatch in
{ pb with
tomatch = Abstract d :: tomatch;
- pred = option_app (generalize_predicate current i d) pb'.pred }
+ pred = option_map (generalize_predicate current i d) pb'.pred }
(* No more patterns: typing the right-hand-side of equations *)
let build_leaf pb =
@@ -1182,7 +1182,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_app (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 }
@@ -1252,7 +1252,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_app (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 }
@@ -1324,7 +1324,7 @@ and compile_generalization pb d rest =
{ pb with
env = push_rel d pb.env;
tomatch = rest;
- pred = option_app ungeneralize_predicate pb.pred;
+ pred = option_map ungeneralize_predicate pb.pred;
mat = List.map (push_rels_eqn [d]) pb.mat } in
let patstat,j = compile pb in
patstat,
@@ -1350,7 +1350,7 @@ and compile_alias pb (deppat,nondeppat,d,t) rest =
{pb with
env = newenv;
tomatch = tomatch;
- pred = option_app (lift_predicate n) pb.pred;
+ pred = option_map (lift_predicate n) pb.pred;
history = history;
mat = mat } in
let patstat,j = compile pb in
@@ -1538,7 +1538,7 @@ let extract_arity_signature env0 tomatchl tmsign =
match tm with
| NotInd (bo,typ) ->
(match t with
- | None -> [na,option_app (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"))
@@ -1610,7 +1610,7 @@ let prepare_predicate loc typing_fun isevars 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_app (fun tycon ->
+ option_map (fun tycon ->
isevars := Coercion.inh_conv_coerces_to loc env !isevars predcclj.uj_val tycon)
tycon
in
diff --git a/pretyping/clenv.ml b/pretyping/clenv.ml
index d7c8a6dd0..b593411ea 100644
--- a/pretyping/clenv.ml
+++ b/pretyping/clenv.ml
@@ -84,10 +84,10 @@ let clenv_environments evd bound c =
let dep = dependent (mkRel 1) c2 in
let na' = if dep then na else Anonymous in
let e' = meta_declare mv c1 ~name:na' e in
- clrec (e', (mkMeta mv)::metas) (option_app ((+) (-1)) n)
+ clrec (e', (mkMeta mv)::metas) (option_map ((+) (-1)) n)
(if dep then (subst1 (mkMeta mv) c2) else c2)
| (n, LetIn (na,b,_,c)) ->
- clrec (e,metas) (option_app ((+) (-1)) n) (subst1 b c)
+ clrec (e,metas) (option_map ((+) (-1)) n) (subst1 b c)
| (n, _) -> (e, List.rev metas, c)
in
clrec (evd,[]) bound c
@@ -100,10 +100,10 @@ let clenv_environments_evars env evd bound c =
| (n, Prod (na,c1,c2)) ->
let e',constr = Evarutil.new_evar e env c1 in
let dep = dependent (mkRel 1) c2 in
- clrec (e', constr::ts) (option_app ((+) (-1)) n)
+ clrec (e', constr::ts) (option_map ((+) (-1)) n)
(if dep then (subst1 constr c2) else c2)
| (n, LetIn (na,b,_,c)) ->
- clrec (e,ts) (option_app ((+) (-1)) n) (subst1 b c)
+ clrec (e,ts) (option_map ((+) (-1)) n) (subst1 b c)
| (n, _) -> (e, List.rev ts, c)
in
clrec (evd,[]) bound c
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index aa4a200e7..1b128e43a 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -168,7 +168,7 @@ module Default = 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_app (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' ->
@@ -184,7 +184,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_app (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 *)
@@ -201,7 +201,7 @@ module Default = struct
let (evd'', v2', t2') =
let v2 =
match v with
- Some v -> option_app (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
@@ -212,7 +212,7 @@ module Default = struct
in
inh_conv_coerce_to_fail loc env1 evd' v2 t2 u2
in
- (evd'', option_app (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 6789459e8..25cf2aedd 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -305,7 +305,7 @@ let detype_case computable detype detype_eqns testdep avoid data p c bl =
then
Anonymous, None, None
else
- match option_app 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
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 2c5a0f901..9f4f1def1 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -41,7 +41,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_app (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 0e3b8f62b..2785d0838 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -209,7 +209,7 @@ let push_rel_context_to_named_context env =
let id = next_name_away na avoid in
((mkVar id)::subst,
id::avoid,
- push_named (id,option_app (substl subst) c,
+ push_named (id,option_map (substl subst) c,
type_app (substl subst) t)
env))
(rel_context env) ~init:([],ids_of_named_context (named_context env),env)
@@ -679,7 +679,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_app (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/pattern.ml b/pretyping/pattern.ml
index 9029578cd..5b3eafb30 100644
--- a/pretyping/pattern.ml
+++ b/pretyping/pattern.ml
@@ -152,7 +152,7 @@ let rec inst lvar = function
| PProd (n,a,b) -> PProd (n,inst lvar a,inst lvar b)
| PLetIn (n,a,b) -> PLetIn (n,inst lvar a,inst lvar b)
| PCase (ci,po,p,pl) ->
- PCase (ci,option_app (inst lvar) po,inst lvar p,Array.map (inst lvar) pl)
+ PCase (ci,option_map (inst lvar) po,inst lvar p,Array.map (inst lvar) pl)
(* Non recursive *)
| (PEvar _ | PRel _ | PRef _ | PSort _ | PMeta _ as x) -> x
(* Bound to terms *)
diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml
index a0f69e701..19e86998f 100644
--- a/pretyping/pretype_errors.ml
+++ b/pretyping/pretype_errors.ml
@@ -59,7 +59,7 @@ let env_ise sigma env =
Sign.fold_rel_context
(fun (na,b,ty) e ->
push_rel
- (na, option_app (nf_evar sigma) b, nf_evar sigma ty)
+ (na, option_map (nf_evar sigma) b, nf_evar sigma ty)
e)
ctxt
~init:env0
@@ -75,7 +75,7 @@ let contract env lc =
env
| _ ->
let t' = substl !l t in
- let c' = option_app (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/pretyping.ml b/pretyping/pretyping.ml
index 64ea0bbb8..82a45ad44 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -385,7 +385,7 @@ module Pretyping_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_app
+ option_map
(fun (abs, ty) ->
match abs with
None ->
@@ -401,7 +401,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct
apply_rec env (n+1)
{ uj_val = nf_isevar !isevars value;
uj_type = nf_isevar !isevars typ' }
- (option_app (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
@@ -409,7 +409,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct
(join_loc floc argloc) env (evars_of !isevars)
resj [hj]
in
- let ftycon = option_app (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/pretyping/rawterm.ml b/pretyping/rawterm.ml
index 86ed95106..0fafb916d 100644
--- a/pretyping/rawterm.ml
+++ b/pretyping/rawterm.ml
@@ -96,7 +96,7 @@ let cases_predicate_names tml =
- boolean in POldCase means it is recursive
i*)
-let map_rawdecl f (na,obd,ty) = (na,option_app 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)
@@ -105,13 +105,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_app 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_app 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_app 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)
@@ -144,7 +144,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_app (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 b3180b06b..983f58f9c 100644
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -67,7 +67,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_app 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 10322c156..4e9a36f2e 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_app (lift n) v
+ option_map (lift n) v
| EvalEvar ev -> Evd.existential_opt_value sigma ev
exception NotEvaluable
diff --git a/pretyping/termops.ml b/pretyping/termops.ml
index 597ddac57..faf91247e 100644
--- a/pretyping/termops.ml
+++ b/pretyping/termops.ml
@@ -961,7 +961,7 @@ let assums_of_rel_context sign =
let lift_rel_context n sign =
let rec liftrec k = function
| (na,c,t)::sign ->
- (na,option_app (liftn n k) c,type_app (liftn n k) t)
+ (na,option_map (liftn n k) c,type_app (liftn n k) t)
::(liftrec (k-1) sign)
| [] -> []
in
diff --git a/tactics/auto.ml b/tactics/auto.ml
index edda5c25b..f7ae4311c 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -778,7 +778,7 @@ let gen_auto n lems dbnames =
| None -> full_auto n lems
| Some l -> auto n lems l
-let inj_or_var = option_app (fun n -> Genarg.ArgArg n)
+let inj_or_var = option_map (fun n -> Genarg.ArgArg n)
let h_auto n lems l =
Refiner.abstract_tactic (TacAuto (inj_or_var n,lems,l)) (gen_auto n lems l)
diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4
index bea6f3303..598a6fe0a 100644
--- a/tactics/eauto.ml4
+++ b/tactics/eauto.ml4
@@ -107,7 +107,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_app Tacinterp.eval_tactic t) ]
+| [ "econstructor" tactic_opt(t) ] -> [ e_any_constructor (option_map Tacinterp.eval_tactic t) ]
END
TACTIC EXTEND eleft
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index 97aeedc6b..1c0e04276 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -80,7 +80,7 @@ END
TACTIC EXTEND replace
| ["replace" constr(c1) "with" constr(c2) in_arg_hyp(in_hyp) by_arg_tac(tac) ] ->
- [ new_replace c1 c2 in_hyp (Util.option_app Tacinterp.eval_tactic tac) ]
+ [ new_replace c1 c2 in_hyp (Util.option_map Tacinterp.eval_tactic tac) ]
END
(* Julien:
diff --git a/tactics/hiddentac.ml b/tactics/hiddentac.ml
index 73259b5ff..e0fd138c2 100644
--- a/tactics/hiddentac.ml
+++ b/tactics/hiddentac.ml
@@ -23,7 +23,7 @@ let inj_id id = (dummy_loc,id)
(* Basic tactics *)
let h_intro_move x y =
- abstract_tactic (TacIntroMove (x, option_app 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
diff --git a/tactics/nbtermdn.ml b/tactics/nbtermdn.ml
index cb042d425..d53ca6126 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_app 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_app 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_app 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 83f7f39bb..7b4c5b8db 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_app (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
@@ -295,9 +295,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_app (subst_mps subst) relation.rel_refl in
- let rel_sym' = option_app (subst_mps subst) relation.rel_sym in
- let rel_trans' = option_app (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
@@ -638,9 +638,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_app (fun c -> mkApp (c,subst)) rel.rel_refl ;
- rel_sym = option_app (fun c -> mkApp (c,subst)) rel.rel_sym;
- rel_trans = option_app (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 =
@@ -1078,9 +1078,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_app (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_app (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
@@ -1134,8 +1134,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 =
- int_add_relation id (constr_of a) (constr_of aeq) (option_app constr_of refl)
- (option_app constr_of sym) (option_app 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 f24297cf0..2eb2d88f4 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -514,7 +514,7 @@ let intern_redexp 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_app (intern_constr_occurrence ist) o)
+ | Simpl o -> Simpl (option_map (intern_constr_occurrence ist) o)
| (Red _ | Hnf | ExtraRedExpr _ | CbvVm as r ) -> r
@@ -523,7 +523,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_app (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)
@@ -618,29 +618,29 @@ 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_app (intern_ident lf ist) ido,
- option_app (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)
| TacApply cb -> TacApply (intern_constr_with_bindings ist cb)
| TacElim (cb,cbo) ->
TacElim (intern_constr_with_bindings ist cb,
- option_app (intern_constr_with_bindings ist) cbo)
+ option_map (intern_constr_with_bindings ist) cbo)
| TacElimType c -> TacElimType (intern_type ist c)
| TacCase cb -> TacCase (intern_constr_with_bindings ist cb)
| TacCaseType c -> TacCaseType (intern_type ist c)
- | TacFix (idopt,n) -> TacFix (option_app (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_app (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_app (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)
@@ -660,26 +660,26 @@ 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_app (intern_int_or_var ist) n,
+ TacAuto (option_map (intern_int_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) -> TacDAuto (option_app (intern_int_or_var ist) n,p)
+ | TacDAuto (n,p) -> TacDAuto (option_map (intern_int_or_var ist) n,p)
(* Derived basic tactics *)
| TacSimpleInduction h ->
TacSimpleInduction (intern_quantified_hypothesis ist h)
| TacNewInduction (lc,cbo,ids) ->
TacNewInduction (List.map (intern_induction_arg ist) lc,
- option_app (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 (c,cbo,ids) ->
TacNewDestruct (List.map (intern_induction_arg ist) c,
- option_app (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
@@ -703,14 +703,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_app (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_redexp ist r, clause_app (intern_hyp_location ist) cl)
| TacChange (occl,c,cl) ->
- TacChange (option_app (intern_constr_occurrence ist) occl,
+ TacChange (option_map (intern_constr_occurrence ist) occl,
intern_constr ist c, clause_app (intern_hyp_location ist) cl)
(* Equivalence relations *)
@@ -750,7 +750,7 @@ and intern_tactic_seq ist = function
| TacLetIn (l,u) ->
let l = List.map
(fun (n,c,b) ->
- (n,option_app (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)
@@ -1124,7 +1124,7 @@ let interp_evaluable ist env = function
let interp_hyp_location ist gl (id,occs,hl) = (interp_hyp ist gl id,occs,hl)
let interp_clause ist gl { onhyps=ol; onconcl=b; concl_occs=occs } =
- { onhyps=option_app(List.map (interp_hyp_location ist gl)) ol;
+ { onhyps=option_map(List.map (interp_hyp_location ist gl)) ol;
onconcl=b;
concl_occs=occs }
@@ -1271,7 +1271,7 @@ let redexp_interp 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_app (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_redexp_interp ist gl = redexp_interp ist (project gl) (pf_env gl)
@@ -1719,23 +1719,23 @@ and interp_atomic ist gl = function
| TacIntrosUntil hyp ->
h_intros_until (interp_quantified_hypothesis ist hyp)
| TacIntroMove (ido,ido') ->
- h_intro_move (option_app (interp_ident ist) ido)
- (option_app (interp_hyp ist gl) ido')
+ h_intro_move (option_map (interp_ident ist) 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)
| TacApply cb -> h_apply (interp_constr_with_bindings ist gl cb)
| TacElim (cb,cbo) ->
h_elim (interp_constr_with_bindings ist gl cb)
- (option_app (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 cb -> h_case (interp_constr_with_bindings ist gl cb)
| TacCaseType c -> h_case_type (pf_interp_type ist gl c)
- | TacFix (idopt,n) -> h_fix (option_app (interp_ident ist) idopt) n
+ | TacFix (idopt,n) -> h_fix (option_map (interp_ident ist) idopt) n
| TacMutualFix (id,n,l) ->
let f (id,n,c) = (interp_ident ist id,n,pf_interp_type ist gl c) in
h_mutual_fix (interp_ident ist id) n (List.map f l)
- | TacCofix idopt -> h_cofix (option_app (interp_ident ist) idopt)
+ | TacCofix idopt -> h_cofix (option_map (interp_ident ist) idopt)
| TacMutualCofix (id,l) ->
let f (id,c) = (interp_ident ist id,pf_interp_type ist gl c) in
h_mutual_cofix (interp_ident ist id) (List.map f l)
@@ -1743,7 +1743,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,c))
- (Tactics.forward (option_app (interp_tactic ist) t)
+ (Tactics.forward (option_map (interp_tactic ist) t)
(interp_intro_pattern ist ipat) c)
| TacGeneralize cl -> h_generalize (List.map (pf_interp_constr ist gl) cl)
| TacGeneralizeDep c -> h_generalize_dep (pf_interp_constr ist gl c)
@@ -1760,29 +1760,29 @@ and interp_atomic ist gl = function
(* Automation tactics *)
| TacTrivial (lems,l) ->
Auto.h_trivial (List.map (pf_interp_constr ist gl) lems)
- (option_app (List.map (interp_hint_base ist)) l)
+ (option_map (List.map (interp_hint_base ist)) l)
| TacAuto (n,lems,l) ->
- Auto.h_auto (option_app (interp_int_or_var ist) n)
+ Auto.h_auto (option_map (interp_int_or_var ist) n)
(List.map (pf_interp_constr ist gl) lems)
- (option_app (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) -> Auto.h_dauto (option_app (interp_int_or_var ist) n,p)
+ | TacDAuto (n,p) -> Auto.h_dauto (option_map (interp_int_or_var ist) n,p)
(* Derived basic tactics *)
| TacSimpleInduction h ->
h_simple_induction (interp_quantified_hypothesis ist h)
| TacNewInduction (lc,cbo,ids) ->
h_new_induction (List.map (interp_induction_arg ist gl) lc)
- (option_app (interp_constr_with_bindings ist gl) cbo)
+ (option_map (interp_constr_with_bindings ist gl) cbo)
(interp_intro_pattern ist ids)
| TacSimpleDestruct h ->
h_simple_destruct (interp_quantified_hypothesis ist h)
| TacNewDestruct (c,cbo,ids) ->
h_new_destruct (List.map (interp_induction_arg ist gl) c)
- (option_app (interp_constr_with_bindings ist gl) cbo)
+ (option_map (interp_constr_with_bindings ist gl) cbo)
(interp_intro_pattern ist ids)
| TacDoubleInduction (h1,h2) ->
let h1 = interp_quantified_hypothesis ist h1 in
@@ -1811,7 +1811,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_app (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)
@@ -1819,7 +1819,7 @@ and interp_atomic ist gl = function
| TacReduce (r,cl) ->
h_reduce (pf_redexp_interp ist gl r) (interp_clause ist gl cl)
| TacChange (occl,c,cl) ->
- h_change (option_app (pf_interp_pattern ist gl) occl)
+ h_change (option_map (pf_interp_pattern ist gl) occl)
(pf_interp_constr ist gl c) (interp_clause ist gl cl)
(* Equivalence relations *)
@@ -1829,7 +1829,7 @@ and interp_atomic ist gl = function
(* Equality and inversion *)
| TacInversion (DepInversion (k,c,ids),hyp) ->
- Inv.dinv k (option_app (pf_interp_constr ist gl) c)
+ Inv.dinv k (option_map (pf_interp_constr ist gl) c)
(interp_intro_pattern ist ids)
(interp_declared_or_quantified_hypothesis ist gl hyp)
| TacInversion (NonDepInversion (k,idl,ids),hyp) ->
@@ -1977,7 +1977,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_app (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
@@ -2005,7 +2005,7 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with
| TacApply cb -> TacApply (subst_raw_with_bindings subst cb)
| TacElim (cb,cbo) ->
TacElim (subst_raw_with_bindings subst cb,
- option_app (subst_raw_with_bindings subst) cbo)
+ option_map (subst_raw_with_bindings subst) cbo)
| TacElimType c -> TacElimType (subst_rawconstr subst c)
| TacCase cb -> TacCase (subst_raw_with_bindings subst cb)
| TacCaseType c -> TacCaseType (subst_rawconstr subst c)
@@ -2035,11 +2035,11 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with
| TacSimpleInduction h as x -> x
| TacNewInduction (lc,cbo,ids) -> (* Pierre C. est-ce correct? *)
TacNewInduction (List.map (subst_induction_arg subst) lc,
- option_app (subst_raw_with_bindings subst) cbo, ids)
+ option_map (subst_raw_with_bindings subst) cbo, ids)
| TacSimpleDestruct h as x -> x
| TacNewDestruct (c,cbo,ids) ->
TacNewDestruct (List.map (subst_induction_arg subst) c, (* Julien F. est-ce correct? *)
- option_app (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)
@@ -2059,13 +2059,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_app (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_app (subst_constr_occurrence subst) occl,
+ TacChange (option_map (subst_constr_occurrence subst) occl,
subst_rawconstr subst c, cl)
(* Equivalence relations *)
@@ -2074,7 +2074,7 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with
(* Equality and inversion *)
| TacInversion (DepInversion (k,c,l),hyp) ->
- TacInversion (DepInversion (k,option_app (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)
@@ -2093,7 +2093,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_app (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/toplevel/minicoq.ml b/toplevel/minicoq.ml
index a92235252..19fd343e5 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_app (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;
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-13 11:39:13 +0000