diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/auto.ml | 6 | ||||
| -rw-r--r-- | tactics/decl_interp.ml | 10 | ||||
| -rw-r--r-- | tactics/eauto.ml4 | 4 | ||||
| -rw-r--r-- | tactics/extraargs.ml4 | 2 | ||||
| -rw-r--r-- | tactics/extratactics.ml4 | 18 | ||||
| -rw-r--r-- | tactics/hiddentac.ml | 12 | ||||
| -rw-r--r-- | tactics/inv.ml | 2 | ||||
| -rw-r--r-- | tactics/nbtermdn.ml | 6 | ||||
| -rw-r--r-- | tactics/setoid_replace.ml | 28 | ||||
| -rw-r--r-- | tactics/tacinterp.ml | 84 | ||||
| -rw-r--r-- | tactics/tactics.ml | 4 |
11 files changed, 88 insertions, 88 deletions
diff --git a/tactics/auto.ml b/tactics/auto.ml index a3ac17b342..8bce850dbb 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -297,7 +297,7 @@ let subst_autohint (_,subst,(local,name,hintlist as obj)) = let trans_clenv clenv = Clenv.subst_clenv subst clenv in let trans_data data code = { data with - pat = option_smartmap (subst_pattern subst) data.pat ; + pat = Option.smartmap (subst_pattern subst) data.pat ; code = code ; } in @@ -637,7 +637,7 @@ and my_find_search db_list local_db hdc concl = (trivial_fail_db db_list local_db) | Unfold_nth c -> unfold_in_concl [[],c] | Extern tacast -> - conclPattern concl (out_some p) tacast)) + conclPattern concl (Option.get p) tacast)) tacl and trivial_resolve db_list local_db cl = @@ -781,7 +781,7 @@ let gen_auto n lems dbnames = | None -> full_auto n lems | Some l -> auto n lems l -let inj_or_var = option_map (fun n -> ArgArg n) +let inj_or_var = Option.map (fun n -> ArgArg n) let h_auto n lems l = Refiner.abstract_tactic (TacAuto (inj_or_var n,List.map inj_open lems,l)) diff --git a/tactics/decl_interp.ml b/tactics/decl_interp.ml index ec8a38501b..771dbe7363 100644 --- a/tactics/decl_interp.ml +++ b/tactics/decl_interp.ml @@ -25,10 +25,10 @@ open Pp let raw_app (loc,hd,args) = if args =[] then hd else RApp(loc,hd,args) let intern_justification_items globs = - option_map (List.map (intern_constr globs)) + Option.map (List.map (intern_constr globs)) let intern_justification_method globs = - option_map (intern_tactic globs) + Option.map (intern_tactic globs) let intern_statement intern_it globs st = {st_label=st.st_label; @@ -52,7 +52,7 @@ let add_name nam globs= let intern_hyp iconstr globs = function Hvar (loc,(id,topt)) -> add_var id globs, - Hvar (loc,(id,option_map (intern_constr globs) topt)) + Hvar (loc,(id,Option.map (intern_constr globs) topt)) | Hprop st -> add_name st.st_label globs, Hprop (intern_statement iconstr globs st) @@ -73,7 +73,7 @@ let intern_casee globs = function let intern_hyp_list args globs = let intern_one globs (loc,(id,opttyp)) = (add_var id globs), - (loc,(id,option_map (intern_constr globs) opttyp)) in + (loc,(id,Option.map (intern_constr globs) opttyp)) in list_fold_map intern_one globs args let intern_suffices_clause globs (hyps,c) = @@ -141,7 +141,7 @@ let rec intern_proof_instr globs instr= (* INTERP *) let interp_justification_items sigma env = - option_map (List.map (fun c ->understand sigma env (fst c))) + Option.map (List.map (fun c ->understand sigma env (fst c))) let interp_constr check_sort sigma env c = if check_sort then diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4 index b62bf5820c..7a6b07d383 100644 --- a/tactics/eauto.ml4 +++ b/tactics/eauto.ml4 @@ -94,7 +94,7 @@ let e_split = e_constructor_tac (Some 1) 1 TACTIC EXTEND econstructor [ "econstructor" integer(n) "with" bindings(c) ] -> [ e_constructor_tac None n c ] | [ "econstructor" integer(n) ] -> [ e_constructor_tac None n NoBindings ] -| [ "econstructor" tactic_opt(t) ] -> [ e_any_constructor (option_map Tacinterp.eval_tactic t) ] +| [ "econstructor" tactic_opt(t) ] -> [ e_any_constructor (Option.map Tacinterp.eval_tactic t) ] END TACTIC EXTEND eleft @@ -192,7 +192,7 @@ and e_my_find_search db_list local_db hdc concl = (e_trivial_fail_db db_list local_db) | Unfold_nth c -> unfold_in_concl [[],c] | Extern tacast -> conclPattern concl - (out_some p) tacast + (Option.get p) tacast in (tac,fmt_autotactic t)) (*i diff --git a/tactics/extraargs.ml4 b/tactics/extraargs.ml4 index 4a6c2ffb25..48d4afbc11 100644 --- a/tactics/extraargs.ml4 +++ b/tactics/extraargs.ml4 @@ -221,7 +221,7 @@ END let gen_in_arg_hyp_to_clause trad_id (hyps ,concl) : Tacticals.clause = {Tacexpr.onhyps= - Util.option_map + Option.map (fun l -> List.map (fun id -> ( ([],trad_id id) ,Tacexpr.InHyp)) diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4 index 787847400b..3ddb4188bf 100644 --- a/tactics/extratactics.ml4 +++ b/tactics/extratactics.ml4 @@ -23,7 +23,7 @@ open Equality TACTIC EXTEND replace ["replace" constr(c1) "with" constr(c2) in_arg_hyp(in_hyp) by_arg_tac(tac) ] --> [ replace_in_clause_maybe_by c1 c2 (glob_in_arg_hyp_to_clause in_hyp) (Util.option_map Tacinterp.eval_tactic tac) ] +-> [ replace_in_clause_maybe_by c1 c2 (glob_in_arg_hyp_to_clause in_hyp) (Option.map Tacinterp.eval_tactic tac) ] END TACTIC EXTEND replace_term_left @@ -152,21 +152,21 @@ open Setoid_replace TACTIC EXTEND setoid_replace [ "setoid_replace" constr(c1) "with" constr(c2) by_arg_tac(tac)] -> - [ setoid_replace (Util.option_map Tacinterp.eval_tactic tac) None c1 c2 ~new_goals:[] ] + [ setoid_replace (Option.map Tacinterp.eval_tactic tac) None c1 c2 ~new_goals:[] ] | [ "setoid_replace" constr(c1) "with" constr(c2) "using" "relation" constr(rel) by_arg_tac(tac)] -> - [ setoid_replace (Util.option_map Tacinterp.eval_tactic tac) (Some rel) c1 c2 ~new_goals:[] ] + [ setoid_replace (Option.map Tacinterp.eval_tactic tac) (Some rel) c1 c2 ~new_goals:[] ] | [ "setoid_replace" constr(c1) "with" constr(c2) "generate" "side" "conditions" constr_list(l) by_arg_tac(tac) ] -> - [ setoid_replace (Util.option_map Tacinterp.eval_tactic tac) None c1 c2 ~new_goals:l ] + [ setoid_replace (Option.map Tacinterp.eval_tactic tac) None c1 c2 ~new_goals:l ] | [ "setoid_replace" constr(c1) "with" constr(c2) "using" "relation" constr(rel) "generate" "side" "conditions" constr_list(l) by_arg_tac(tac) ] -> - [ setoid_replace (Util.option_map Tacinterp.eval_tactic tac) (Some rel) c1 c2 ~new_goals:l ] + [ setoid_replace (Option.map Tacinterp.eval_tactic tac) (Some rel) c1 c2 ~new_goals:l ] | [ "setoid_replace" constr(c1) "with" constr(c2) "in" hyp(h) by_arg_tac(tac) ] -> - [ setoid_replace_in (Util.option_map Tacinterp.eval_tactic tac) h None c1 c2 ~new_goals:[] ] + [ setoid_replace_in (Option.map Tacinterp.eval_tactic tac) h None c1 c2 ~new_goals:[] ] | [ "setoid_replace" constr(c1) "with" constr(c2) "in" hyp(h) "using" "relation" constr(rel) by_arg_tac(tac)] -> - [ setoid_replace_in (Util.option_map Tacinterp.eval_tactic tac) h (Some rel) c1 c2 ~new_goals:[] ] + [ setoid_replace_in (Option.map Tacinterp.eval_tactic tac) h (Some rel) c1 c2 ~new_goals:[] ] | [ "setoid_replace" constr(c1) "with" constr(c2) "in" hyp(h) "generate" "side" "conditions" constr_list(l) by_arg_tac(tac)] -> - [ setoid_replace_in (Util.option_map Tacinterp.eval_tactic tac) h None c1 c2 ~new_goals:l ] + [ setoid_replace_in (Option.map Tacinterp.eval_tactic tac) h None c1 c2 ~new_goals:l ] | [ "setoid_replace" constr(c1) "with" constr(c2) "in" hyp(h) "using" "relation" constr(rel) "generate" "side" "conditions" constr_list(l) by_arg_tac(tac)] -> - [ setoid_replace_in (Util.option_map Tacinterp.eval_tactic tac) h (Some rel) c1 c2 ~new_goals:l ] + [ setoid_replace_in (Option.map Tacinterp.eval_tactic tac) h (Some rel) c1 c2 ~new_goals:l ] END TACTIC EXTEND setoid_rewrite diff --git a/tactics/hiddentac.ml b/tactics/hiddentac.ml index 8bb7c5c2ce..f5c54a5336 100644 --- a/tactics/hiddentac.ml +++ b/tactics/hiddentac.ml @@ -30,7 +30,7 @@ let inj_occ (occ,c) = (occ,inj_open c) (* Basic tactics *) let h_intro_move x y = - abstract_tactic (TacIntroMove (x, option_map inj_id y)) (intro_move x y) + abstract_tactic (TacIntroMove (x, Option.map inj_id y)) (intro_move x y) let h_intro x = h_intro_move (Some x) None let h_intros_until x = abstract_tactic (TacIntrosUntil x) (intros_until x) let h_assumption = abstract_tactic TacAssumption assumption @@ -43,7 +43,7 @@ let h_apply ev cb = abstract_tactic (TacApply (ev,inj_open_wb cb)) (apply_with_ebindings_gen ev cb) let h_elim ev cb cbo = - abstract_tactic (TacElim (ev,inj_open_wb cb,option_map inj_open_wb cbo)) + abstract_tactic (TacElim (ev,inj_open_wb cb,Option.map inj_open_wb cbo)) (elim ev cb cbo) let h_elim_type c = abstract_tactic (TacElimType (inj_open c)) (elim_type c) let h_case ev cb = abstract_tactic (TacCase (ev,inj_open_wb cb)) (general_case_analysis ev cb) @@ -78,10 +78,10 @@ let h_simple_induction h = let h_simple_destruct h = abstract_tactic (TacSimpleDestruct h) (simple_destruct h) let h_new_induction ev c e idl = - abstract_tactic (TacNewInduction (ev,List.map inj_ia c,option_map inj_open_wb e,idl)) + abstract_tactic (TacNewInduction (ev,List.map inj_ia c,Option.map inj_open_wb e,idl)) (new_induct ev c e idl) let h_new_destruct ev c e idl = - abstract_tactic (TacNewDestruct (ev,List.map inj_ia c,option_map inj_open_wb e,idl)) + abstract_tactic (TacNewDestruct (ev,List.map inj_ia c,Option.map inj_open_wb e,idl)) (new_destruct ev c e idl) let h_specialize n d = abstract_tactic (TacSpecialize (n,inj_open_wb d)) (new_hyp n d) let h_lapply c = abstract_tactic (TacLApply (inj_open c)) (cut_and_apply c) @@ -113,8 +113,8 @@ let h_simplest_right = h_right NoBindings let h_reduce r cl = abstract_tactic (TacReduce (inj_red_expr r,cl)) (reduce r cl) let h_change oc c cl = - abstract_tactic (TacChange (option_map inj_occ oc,inj_open c,cl)) - (change (option_map Redexpr.out_with_occurrences oc) c cl) + abstract_tactic (TacChange (Option.map inj_occ oc,inj_open c,cl)) + (change (Option.map Redexpr.out_with_occurrences oc) c cl) (* Equivalence relations *) let h_reflexivity = abstract_tactic TacReflexivity intros_reflexivity diff --git a/tactics/inv.ml b/tactics/inv.ml index bfaa7e5e48..d8d7661be7 100644 --- a/tactics/inv.ml +++ b/tactics/inv.ml @@ -385,7 +385,7 @@ let rec get_names allow_conj = function | IntroOrAndPattern [l] -> if allow_conj then if l = [] then (None,[]) else - let l = List.map (fun id -> out_some (fst (get_names false id))) l in + let l = List.map (fun id -> Option.get (fst (get_names false id))) l in (Some (List.hd l), l) else error "Nested conjunctive patterns not allowed for inversion equations" diff --git a/tactics/nbtermdn.ml b/tactics/nbtermdn.ml index d53ca6126e..c53a5088a9 100644 --- a/tactics/nbtermdn.ml +++ b/tactics/nbtermdn.ml @@ -43,14 +43,14 @@ let get_dn dnm hkey = try Gmap.find hkey dnm with Not_found -> Btermdn.create () let add dn (na,(pat,valu)) = - let hkey = option_map fst (Termdn.constr_pat_discr pat) in + let hkey = Option.map fst (Termdn.constr_pat_discr pat) in dn.table <- Gmap.add na (pat,valu) dn.table; let dnm = dn.patterns in dn.patterns <- Gmap.add hkey (Btermdn.add (get_dn dnm hkey) (pat,valu)) dnm let rmv dn na = let (pat,valu) = Gmap.find na dn.table in - let hkey = option_map fst (Termdn.constr_pat_discr pat) in + let hkey = Option.map fst (Termdn.constr_pat_discr pat) in dn.table <- Gmap.remove na dn.table; let dnm = dn.patterns in dn.patterns <- Gmap.add hkey (Btermdn.rmv (get_dn dnm hkey) (pat,valu)) dnm @@ -62,7 +62,7 @@ let remap ndn na (pat,valu) = add ndn (na,(pat,valu)) let lookup dn valu = - let hkey = option_map fst (Termdn.constr_val_discr valu) in + let hkey = Option.map fst (Termdn.constr_val_discr valu) in try Btermdn.lookup (Gmap.find hkey dn.patterns) valu with Not_found -> [] let app f dn = Gmap.iter f dn.table diff --git a/tactics/setoid_replace.ml b/tactics/setoid_replace.ml index 36ef9be47a..307968116a 100644 --- a/tactics/setoid_replace.ml +++ b/tactics/setoid_replace.ml @@ -85,7 +85,7 @@ type morphism_class = let subst_mps_in_relation_class subst = function Relation t -> Relation (subst_mps subst t) - | Leibniz t -> Leibniz (option_map (subst_mps subst) t) + | Leibniz t -> Leibniz (Option.map (subst_mps subst) t) let subst_mps_in_argument_class subst (variance,rel) = variance, subst_mps_in_relation_class subst rel @@ -297,9 +297,9 @@ let relation_morphism_of_constr_morphism = let subst_relation subst relation = let rel_a' = subst_mps subst relation.rel_a in let rel_aeq' = subst_mps subst relation.rel_aeq in - let rel_refl' = option_map (subst_mps subst) relation.rel_refl in - let rel_sym' = option_map (subst_mps subst) relation.rel_sym in - let rel_trans' = option_map (subst_mps subst) relation.rel_trans in + let rel_refl' = Option.map (subst_mps subst) relation.rel_refl in + let rel_sym' = Option.map (subst_mps subst) relation.rel_sym in + let rel_trans' = Option.map (subst_mps subst) relation.rel_trans in let rel_X_relation_class' = subst_mps subst relation.rel_X_relation_class in let rel_Xreflexive_relation_class' = subst_mps subst relation.rel_Xreflexive_relation_class @@ -640,9 +640,9 @@ let apply_to_relation subst rel = assert (new_quantifiers_no >= 0) ; { rel_a = mkApp (rel.rel_a, subst) ; rel_aeq = mkApp (rel.rel_aeq, subst) ; - rel_refl = option_map (fun c -> mkApp (c,subst)) rel.rel_refl ; - rel_sym = option_map (fun c -> mkApp (c,subst)) rel.rel_sym; - rel_trans = option_map (fun c -> mkApp (c,subst)) rel.rel_trans; + rel_refl = Option.map (fun c -> mkApp (c,subst)) rel.rel_refl ; + rel_sym = Option.map (fun c -> mkApp (c,subst)) rel.rel_sym; + rel_trans = Option.map (fun c -> mkApp (c,subst)) rel.rel_trans; rel_quantifiers_no = new_quantifiers_no; rel_X_relation_class = mkApp (rel.rel_X_relation_class, subst); rel_Xreflexive_relation_class = @@ -1012,9 +1012,9 @@ let int_add_relation id a aeq refl sym trans = let env = Global.env () in let a_quantifiers_rev = check_a env a in check_eq env a_quantifiers_rev a aeq ; - option_iter (check_refl env a_quantifiers_rev a aeq) refl ; - option_iter (check_sym env a_quantifiers_rev a aeq) sym ; - option_iter (check_trans env a_quantifiers_rev a aeq) trans ; + Option.iter (check_refl env a_quantifiers_rev a aeq) refl ; + Option.iter (check_sym env a_quantifiers_rev a aeq) sym ; + Option.iter (check_trans env a_quantifiers_rev a aeq) trans ; let quantifiers_no = List.length a_quantifiers_rev in let aeq_rel = { rel_a = a; @@ -1075,9 +1075,9 @@ let int_add_relation id a aeq refl sym trans = let a_instance = apply_to_rels a a_quantifiers_rev in let aeq_instance = apply_to_rels aeq a_quantifiers_rev in let sym_instance = - option_map (fun x -> apply_to_rels x a_quantifiers_rev) sym in + Option.map (fun x -> apply_to_rels x a_quantifiers_rev) sym in let refl_instance = - option_map (fun x -> apply_to_rels x a_quantifiers_rev) refl in + Option.map (fun x -> apply_to_rels x a_quantifiers_rev) refl in let trans_instance = apply_to_rels trans a_quantifiers_rev in let aeq_rel_class_and_var1, aeq_rel_class_and_var2, lemma, output = match sym_instance, refl_instance with @@ -1132,8 +1132,8 @@ let int_add_relation id a aeq refl sym trans = (* The vernac command "Add Relation ..." *) let add_relation id a aeq refl sym trans = Coqlib.check_required_library ["Coq";"Setoids";"Setoid_tac"]; - int_add_relation id (constr_of a) (constr_of aeq) (option_map constr_of refl) - (option_map constr_of sym) (option_map constr_of trans) + int_add_relation id (constr_of a) (constr_of aeq) (Option.map constr_of refl) + (Option.map constr_of sym) (Option.map constr_of trans) (************************ Add Setoid ******************************************) diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 11d86630bc..09d9fe8d79 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -550,7 +550,7 @@ let intern_red_expr ist = function | Cbv f -> Cbv (intern_flag ist f) | Lazy f -> Lazy (intern_flag ist f) | Pattern l -> Pattern (List.map (intern_constr_occurrence ist) l) - | Simpl o -> Simpl (option_map (intern_constr_occurrence ist) o) + | Simpl o -> Simpl (Option.map (intern_constr_occurrence ist) o) | (Red _ | Hnf | ExtraRedExpr _ | CbvVm as r ) -> r @@ -559,7 +559,7 @@ let intern_inversion_strength lf ist = function NonDepInversion (k,List.map (intern_hyp_or_metaid ist) idl, intern_intro_pattern lf ist ids) | DepInversion (k,copt,ids) -> - DepInversion (k, option_map (intern_constr ist) copt, + DepInversion (k, Option.map (intern_constr ist) copt, intern_intro_pattern lf ist ids) | InversionUsing (c,idl) -> InversionUsing (intern_constr ist c, List.map (intern_hyp_or_metaid ist) idl) @@ -654,8 +654,8 @@ let rec intern_atomic lf ist x = TacIntroPattern (List.map (intern_intro_pattern lf ist) l) | TacIntrosUntil hyp -> TacIntrosUntil (intern_quantified_hypothesis ist hyp) | TacIntroMove (ido,ido') -> - TacIntroMove (option_map (intern_ident lf ist) ido, - option_map (intern_hyp ist) ido') + TacIntroMove (Option.map (intern_ident lf ist) ido, + Option.map (intern_hyp ist) ido') | TacAssumption -> TacAssumption | TacExact c -> TacExact (intern_constr ist c) | TacExactNoCheck c -> TacExactNoCheck (intern_constr ist c) @@ -663,21 +663,21 @@ let rec intern_atomic lf ist x = | TacApply (ev,cb) -> TacApply (ev,intern_constr_with_bindings ist cb) | TacElim (ev,cb,cbo) -> TacElim (ev,intern_constr_with_bindings ist cb, - option_map (intern_constr_with_bindings ist) cbo) + Option.map (intern_constr_with_bindings ist) cbo) | TacElimType c -> TacElimType (intern_type ist c) | TacCase (ev,cb) -> TacCase (ev,intern_constr_with_bindings ist cb) | TacCaseType c -> TacCaseType (intern_type ist c) - | TacFix (idopt,n) -> TacFix (option_map (intern_ident lf ist) idopt,n) + | TacFix (idopt,n) -> TacFix (Option.map (intern_ident lf ist) idopt,n) | TacMutualFix (id,n,l) -> let f (id,n,c) = (intern_ident lf ist id,n,intern_type ist c) in TacMutualFix (intern_ident lf ist id, n, List.map f l) - | TacCofix idopt -> TacCofix (option_map (intern_ident lf ist) idopt) + | TacCofix idopt -> TacCofix (Option.map (intern_ident lf ist) idopt) | TacMutualCofix (id,l) -> let f (id,c) = (intern_ident lf ist id,intern_type ist c) in TacMutualCofix (intern_ident lf ist id, List.map f l) | TacCut c -> TacCut (intern_type ist c) | TacAssert (otac,ipat,c) -> - TacAssert (option_map (intern_tactic ist) otac, + TacAssert (Option.map (intern_tactic ist) otac, intern_intro_pattern lf ist ipat, intern_constr_gen (otac<>None) ist c) | TacGeneralize cl -> TacGeneralize (List.map (intern_constr ist) cl) @@ -690,14 +690,14 @@ let rec intern_atomic lf ist x = (* Automation tactics *) | TacTrivial (lems,l) -> TacTrivial (List.map (intern_constr ist) lems,l) | TacAuto (n,lems,l) -> - TacAuto (option_map (intern_or_var ist) n, + TacAuto (Option.map (intern_or_var ist) n, List.map (intern_constr ist) lems,l) | TacAutoTDB n -> TacAutoTDB n | TacDestructHyp (b,id) -> TacDestructHyp(b,intern_hyp ist id) | TacDestructConcl -> TacDestructConcl | TacSuperAuto (n,l,b1,b2) -> TacSuperAuto (n,l,b1,b2) | TacDAuto (n,p,lems) -> - TacDAuto (option_map (intern_or_var ist) n,p, + TacDAuto (Option.map (intern_or_var ist) n,p, List.map (intern_constr ist) lems) (* Derived basic tactics *) @@ -705,13 +705,13 @@ let rec intern_atomic lf ist x = TacSimpleInduction (intern_quantified_hypothesis ist h) | TacNewInduction (ev,lc,cbo,ids) -> TacNewInduction (ev,List.map (intern_induction_arg ist) lc, - option_map (intern_constr_with_bindings ist) cbo, + Option.map (intern_constr_with_bindings ist) cbo, (intern_intro_pattern lf ist ids)) | TacSimpleDestruct h -> TacSimpleDestruct (intern_quantified_hypothesis ist h) | TacNewDestruct (ev,c,cbo,ids) -> TacNewDestruct (ev,List.map (intern_induction_arg ist) c, - option_map (intern_constr_with_bindings ist) cbo, + Option.map (intern_constr_with_bindings ist) cbo, (intern_intro_pattern lf ist ids)) | TacDoubleInduction (h1,h2) -> let h1 = intern_quantified_hypothesis ist h1 in @@ -738,14 +738,14 @@ let rec intern_atomic lf ist x = | TacLeft bl -> TacLeft (intern_bindings ist bl) | TacRight bl -> TacRight (intern_bindings ist bl) | TacSplit (b,bl) -> TacSplit (b,intern_bindings ist bl) - | TacAnyConstructor t -> TacAnyConstructor (option_map (intern_tactic ist) t) + | TacAnyConstructor t -> TacAnyConstructor (Option.map (intern_tactic ist) t) | TacConstructor (n,bl) -> TacConstructor (n, intern_bindings ist bl) (* Conversion *) | TacReduce (r,cl) -> TacReduce (intern_red_expr ist r, clause_app (intern_hyp_location ist) cl) | TacChange (occl,c,cl) -> - TacChange (option_map (intern_constr_occurrence ist) occl, + TacChange (Option.map (intern_constr_occurrence ist) occl, (if occl = None then intern_type ist c else intern_constr ist c), clause_app (intern_hyp_location ist) cl) @@ -791,7 +791,7 @@ and intern_tactic_seq ist = function | TacLetIn (l,u) -> let l = List.map (fun (n,c,b) -> - (n,option_map (intern_tactic ist) c, intern_tacarg !strict_check ist b)) l in + (n,Option.map (intern_tactic ist) c, intern_tacarg !strict_check ist b)) l in let (l1,l2) = ist.ltacvars in let ist' = { ist with ltacvars = ((extract_let_names l)@l1,l2) } in ist.ltacvars, TacLetIn (l,intern_tactic ist' u) @@ -1248,7 +1248,7 @@ let interp_hyp_location ist gl ((occs,id),hl) = ((interp_int_or_var_list ist occs,interp_hyp ist gl id),hl) let interp_clause ist gl { onhyps=ol; onconcl=b; concl_occs=occs } = - { onhyps=option_map(List.map (interp_hyp_location ist gl)) ol; + { onhyps=Option.map(List.map (interp_hyp_location ist gl)) ol; onconcl=b; concl_occs= interp_int_or_var_list ist occs } @@ -1440,7 +1440,7 @@ let interp_red_expr ist sigma env = function | Cbv f -> Cbv (interp_flag ist env f) | Lazy f -> Lazy (interp_flag ist env f) | Pattern l -> Pattern (List.map (interp_pattern ist sigma env) l) - | Simpl o -> Simpl (option_map (interp_pattern ist sigma env) o) + | Simpl o -> Simpl (Option.map (interp_pattern ist sigma env) o) | (Red _ | Hnf | ExtraRedExpr _ | CbvVm as r) -> r let pf_interp_red_expr ist gl = interp_red_expr ist (project gl) (pf_env gl) @@ -2037,8 +2037,8 @@ and interp_atomic ist gl = function | TacIntrosUntil hyp -> h_intros_until (interp_quantified_hypothesis ist hyp) | TacIntroMove (ido,ido') -> - h_intro_move (option_map (interp_fresh_ident ist gl) ido) - (option_map (interp_hyp ist gl) ido') + h_intro_move (Option.map (interp_fresh_ident ist gl) ido) + (Option.map (interp_hyp ist gl) ido') | TacAssumption -> h_assumption | TacExact c -> h_exact (pf_interp_casted_constr ist gl c) | TacExactNoCheck c -> h_exact_no_check (pf_interp_constr ist gl c) @@ -2046,15 +2046,15 @@ and interp_atomic ist gl = function | TacApply (ev,cb) -> h_apply ev (interp_constr_with_bindings ist gl cb) | TacElim (ev,cb,cbo) -> h_elim ev (interp_constr_with_bindings ist gl cb) - (option_map (interp_constr_with_bindings ist gl) cbo) + (Option.map (interp_constr_with_bindings ist gl) cbo) | TacElimType c -> h_elim_type (pf_interp_type ist gl c) | TacCase (ev,cb) -> h_case ev (interp_constr_with_bindings ist gl cb) | TacCaseType c -> h_case_type (pf_interp_type ist gl c) - | TacFix (idopt,n) -> h_fix (option_map (interp_fresh_ident ist gl) idopt) n + | TacFix (idopt,n) -> h_fix (Option.map (interp_fresh_ident ist gl) idopt) n | TacMutualFix (id,n,l) -> let f (id,n,c) = (interp_fresh_ident ist gl id,n,pf_interp_type ist gl c) in h_mutual_fix (interp_fresh_ident ist gl id) n (List.map f l) - | TacCofix idopt -> h_cofix (option_map (interp_fresh_ident ist gl) idopt) + | TacCofix idopt -> h_cofix (Option.map (interp_fresh_ident ist gl) idopt) | TacMutualCofix (id,l) -> let f (id,c) = (interp_fresh_ident ist gl id,pf_interp_type ist gl c) in h_mutual_cofix (interp_fresh_ident ist gl id) (List.map f l) @@ -2062,7 +2062,7 @@ and interp_atomic ist gl = function | TacAssert (t,ipat,c) -> let c = (if t=None then pf_interp_constr else pf_interp_type) ist gl c in abstract_tactic (TacAssert (t,ipat,inj_open c)) - (Tactics.forward (option_map (interp_tactic ist) t) + (Tactics.forward (Option.map (interp_tactic ist) t) (interp_intro_pattern ist gl ipat) c) | TacGeneralize cl -> h_generalize (pf_interp_constr_list ist gl cl) | TacGeneralizeDep c -> h_generalize_dep (pf_interp_constr ist gl c) @@ -2073,17 +2073,17 @@ and interp_atomic ist gl = function (* Automation tactics *) | TacTrivial (lems,l) -> Auto.h_trivial (pf_interp_constr_list ist gl lems) - (option_map (List.map (interp_hint_base ist)) l) + (Option.map (List.map (interp_hint_base ist)) l) | TacAuto (n,lems,l) -> - Auto.h_auto (option_map (interp_int_or_var ist) n) + Auto.h_auto (Option.map (interp_int_or_var ist) n) (pf_interp_constr_list ist gl lems) - (option_map (List.map (interp_hint_base ist)) l) + (Option.map (List.map (interp_hint_base ist)) l) | TacAutoTDB n -> Dhyp.h_auto_tdb n | TacDestructHyp (b,id) -> Dhyp.h_destructHyp b (interp_hyp ist gl id) | TacDestructConcl -> Dhyp.h_destructConcl | TacSuperAuto (n,l,b1,b2) -> Auto.h_superauto n l b1 b2 | TacDAuto (n,p,lems) -> - Auto.h_dauto (option_map (interp_int_or_var ist) n,p) + Auto.h_dauto (Option.map (interp_int_or_var ist) n,p) (pf_interp_constr_list ist gl lems) (* Derived basic tactics *) @@ -2091,13 +2091,13 @@ and interp_atomic ist gl = function h_simple_induction (interp_quantified_hypothesis ist h) | TacNewInduction (ev,lc,cbo,ids) -> h_new_induction ev (List.map (interp_induction_arg ist gl) lc) - (option_map (interp_constr_with_bindings ist gl) cbo) + (Option.map (interp_constr_with_bindings ist gl) cbo) (interp_intro_pattern ist gl ids) | TacSimpleDestruct h -> h_simple_destruct (interp_quantified_hypothesis ist h) | TacNewDestruct (ev,c,cbo,ids) -> h_new_destruct ev (List.map (interp_induction_arg ist gl) c) - (option_map (interp_constr_with_bindings ist gl) cbo) + (Option.map (interp_constr_with_bindings ist gl) cbo) (interp_intro_pattern ist gl ids) | TacDoubleInduction (h1,h2) -> let h1 = interp_quantified_hypothesis ist h1 in @@ -2128,7 +2128,7 @@ and interp_atomic ist gl = function | TacSplit (_,bl) -> h_split (interp_bindings ist gl bl) | TacAnyConstructor t -> abstract_tactic (TacAnyConstructor t) - (Tactics.any_constructor (option_map (interp_tactic ist) t)) + (Tactics.any_constructor (Option.map (interp_tactic ist) t)) | TacConstructor (n,bl) -> h_constructor (skip_metaid n) (interp_bindings ist gl bl) @@ -2136,7 +2136,7 @@ and interp_atomic ist gl = function | TacReduce (r,cl) -> h_reduce (pf_interp_red_expr ist gl r) (interp_clause ist gl cl) | TacChange (occl,c,cl) -> - h_change (option_map (pf_interp_pattern ist gl) occl) + h_change (Option.map (pf_interp_pattern ist gl) occl) (if occl = None then pf_interp_type ist gl c else pf_interp_constr ist gl c) (interp_clause ist gl cl) @@ -2152,7 +2152,7 @@ and interp_atomic ist gl = function (List.map (fun (b,c) -> (b, interp_constr_with_bindings ist gl c)) l) (interp_clause ist gl cl) | TacInversion (DepInversion (k,c,ids),hyp) -> - Inv.dinv k (option_map (pf_interp_constr ist gl) c) + Inv.dinv k (Option.map (pf_interp_constr ist gl) c) (interp_intro_pattern ist gl ids) (interp_declared_or_quantified_hypothesis ist gl hyp) | TacInversion (NonDepInversion (k,idl,ids),hyp) -> @@ -2201,7 +2201,7 @@ and interp_atomic ist gl = function | ExtraArgType s when tactic_genarg_level s <> None -> (* Special treatment of tactic arguments *) val_interp ist gl - (out_gen (globwit_tactic (out_some (tactic_genarg_level s))) x) + (out_gen (globwit_tactic (Option.get (tactic_genarg_level s))) x) | List0ArgType ConstrArgType -> let wit = wit_list0 globwit_constr in VList (List.map (mk_constr_value ist gl) (out_gen wit x)) @@ -2348,7 +2348,7 @@ let subst_redexp subst = function | Cbv f -> Cbv (subst_flag subst f) | Lazy f -> Lazy (subst_flag subst f) | Pattern l -> Pattern (List.map (subst_constr_occurrence subst) l) - | Simpl o -> Simpl (option_map (subst_constr_occurrence subst) o) + | Simpl o -> Simpl (Option.map (subst_constr_occurrence subst) o) | (Red _ | Hnf | ExtraRedExpr _ | CbvVm as r) -> r let subst_raw_may_eval subst = function @@ -2377,7 +2377,7 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with | TacApply (ev,cb) -> TacApply (ev,subst_raw_with_bindings subst cb) | TacElim (ev,cb,cbo) -> TacElim (ev,subst_raw_with_bindings subst cb, - option_map (subst_raw_with_bindings subst) cbo) + Option.map (subst_raw_with_bindings subst) cbo) | TacElimType c -> TacElimType (subst_rawconstr subst c) | TacCase (ev,cb) -> TacCase (ev,subst_raw_with_bindings subst cb) | TacCaseType c -> TacCaseType (subst_rawconstr subst c) @@ -2389,7 +2389,7 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with TacMutualCofix (id, List.map (fun (id,c) -> (id,subst_rawconstr subst c)) l) | TacCut c -> TacCut (subst_rawconstr subst c) | TacAssert (b,na,c) -> - TacAssert (option_map (subst_tactic subst) b,na,subst_rawconstr subst c) + TacAssert (Option.map (subst_tactic subst) b,na,subst_rawconstr subst c) | TacGeneralize cl -> TacGeneralize (List.map (subst_rawconstr subst) cl) | TacGeneralizeDep c -> TacGeneralizeDep (subst_rawconstr subst c) | TacLetTac (id,c,clp) -> TacLetTac (id,subst_rawconstr subst c,clp) @@ -2407,11 +2407,11 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with | TacSimpleInduction h as x -> x | TacNewInduction (ev,lc,cbo,ids) -> TacNewInduction (ev,List.map (subst_induction_arg subst) lc, - option_map (subst_raw_with_bindings subst) cbo, ids) + Option.map (subst_raw_with_bindings subst) cbo, ids) | TacSimpleDestruct h as x -> x | TacNewDestruct (ev,c,cbo,ids) -> TacNewDestruct (ev,List.map (subst_induction_arg subst) c, - option_map (subst_raw_with_bindings subst) cbo, ids) + Option.map (subst_raw_with_bindings subst) cbo, ids) | TacDoubleInduction (h1,h2) as x -> x | TacDecomposeAnd c -> TacDecomposeAnd (subst_rawconstr subst c) | TacDecomposeOr c -> TacDecomposeOr (subst_rawconstr subst c) @@ -2431,13 +2431,13 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with | TacLeft bl -> TacLeft (subst_bindings subst bl) | TacRight bl -> TacRight (subst_bindings subst bl) | TacSplit (b,bl) -> TacSplit (b,subst_bindings subst bl) - | TacAnyConstructor t -> TacAnyConstructor (option_map (subst_tactic subst) t) + | TacAnyConstructor t -> TacAnyConstructor (Option.map (subst_tactic subst) t) | TacConstructor (n,bl) -> TacConstructor (n, subst_bindings subst bl) (* Conversion *) | TacReduce (r,cl) -> TacReduce (subst_redexp subst r, cl) | TacChange (occl,c,cl) -> - TacChange (option_map (subst_constr_occurrence subst) occl, + TacChange (Option.map (subst_constr_occurrence subst) occl, subst_rawconstr subst c, cl) (* Equivalence relations *) @@ -2450,7 +2450,7 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with List.map (fun (b,c) ->b,subst_raw_with_bindings subst c) l, cl) | TacInversion (DepInversion (k,c,l),hyp) -> - TacInversion (DepInversion (k,option_map (subst_rawconstr subst) c,l),hyp) + TacInversion (DepInversion (k,Option.map (subst_rawconstr subst) c,l),hyp) | TacInversion (NonDepInversion _,_) as x -> x | TacInversion (InversionUsing (c,cl),hyp) -> TacInversion (InversionUsing (subst_rawconstr subst c,cl),hyp) @@ -2469,7 +2469,7 @@ and subst_tactic subst (t:glob_tactic_expr) = match t with let lrc = List.map (fun (n,b) -> (n,subst_tactic_fun subst b)) lrc in TacLetRecIn (lrc,(subst_tactic subst u:glob_tactic_expr)) | TacLetIn (l,u) -> - let l = List.map (fun (n,c,b) -> (n,option_map (subst_tactic subst) c,subst_tacarg subst b)) l in + let l = List.map (fun (n,c,b) -> (n,Option.map (subst_tactic subst) c,subst_tacarg subst b)) l in TacLetIn (l,subst_tactic subst u) | TacMatchContext (lz,lr,lmr) -> TacMatchContext(lz,lr, subst_match_rule subst lmr) diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 3121d3a495..782f2a4c15 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -60,7 +60,7 @@ let inj_open c = (Evd.empty,c) let inj_occ (occ,c) = (occ,inj_open c) let inj_red_expr = function - | Simpl lo -> Simpl (option_map inj_occ lo) + | Simpl lo -> Simpl (Option.map inj_occ lo) | Fold l -> Fold (List.map inj_open l) | Pattern l -> Pattern (List.map inj_occ l) | (ExtraRedExpr _ | CbvVm | Red _ | Hnf | Cbv _ | Lazy _ | Unfold _ as c) @@ -1694,7 +1694,7 @@ let mkHRefl t x = [| t; x |]) let mkCoe a x p px y eq = - mkApp (out_some (build_coq_eq_data ()).rect, [| a; x; p; px; y; eq |]) + mkApp (Option.get (build_coq_eq_data ()).rect, [| a; x; p; px; y; eq |]) let lift_togethern n l = let l', _ = |