diff options
author | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-04-27 19:37:33 +0000 |
---|---|---|
committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-04-27 19:37:33 +0000 |
commit | 61d11c649b4cd68e92861e2fea86f6c6a6b5bb6a (patch) | |
tree | ff162856b856b8fa11ac367ecf9bfa4a9de29034 | |
parent | 2ec958c3c8d2942242837787a3941abb14702b5c (diff) |
Standardisation nom option_app en option_map
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8752 85f007b7-540e-0410-9357-904b9bb8a0f7
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; |