diff options
Diffstat (limited to 'tactics/hiddentac.ml')
| -rw-r--r-- | tactics/hiddentac.ml | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/tactics/hiddentac.ml b/tactics/hiddentac.ml index 8bb7c5c2c..f5c54a533 100644 --- a/tactics/hiddentac.ml +++ b/tactics/hiddentac.ml @@ -30,7 +30,7 @@ let inj_occ (occ,c) = (occ,inj_open c) (* Basic tactics *) let h_intro_move x y = - abstract_tactic (TacIntroMove (x, option_map inj_id y)) (intro_move x y) + abstract_tactic (TacIntroMove (x, Option.map inj_id y)) (intro_move x y) let h_intro x = h_intro_move (Some x) None let h_intros_until x = abstract_tactic (TacIntrosUntil x) (intros_until x) let h_assumption = abstract_tactic TacAssumption assumption @@ -43,7 +43,7 @@ let h_apply ev cb = abstract_tactic (TacApply (ev,inj_open_wb cb)) (apply_with_ebindings_gen ev cb) let h_elim ev cb cbo = - abstract_tactic (TacElim (ev,inj_open_wb cb,option_map inj_open_wb cbo)) + abstract_tactic (TacElim (ev,inj_open_wb cb,Option.map inj_open_wb cbo)) (elim ev cb cbo) let h_elim_type c = abstract_tactic (TacElimType (inj_open c)) (elim_type c) let h_case ev cb = abstract_tactic (TacCase (ev,inj_open_wb cb)) (general_case_analysis ev cb) @@ -78,10 +78,10 @@ let h_simple_induction h = let h_simple_destruct h = abstract_tactic (TacSimpleDestruct h) (simple_destruct h) let h_new_induction ev c e idl = - abstract_tactic (TacNewInduction (ev,List.map inj_ia c,option_map inj_open_wb e,idl)) + abstract_tactic (TacNewInduction (ev,List.map inj_ia c,Option.map inj_open_wb e,idl)) (new_induct ev c e idl) let h_new_destruct ev c e idl = - abstract_tactic (TacNewDestruct (ev,List.map inj_ia c,option_map inj_open_wb e,idl)) + abstract_tactic (TacNewDestruct (ev,List.map inj_ia c,Option.map inj_open_wb e,idl)) (new_destruct ev c e idl) let h_specialize n d = abstract_tactic (TacSpecialize (n,inj_open_wb d)) (new_hyp n d) let h_lapply c = abstract_tactic (TacLApply (inj_open c)) (cut_and_apply c) @@ -113,8 +113,8 @@ let h_simplest_right = h_right NoBindings let h_reduce r cl = abstract_tactic (TacReduce (inj_red_expr r,cl)) (reduce r cl) let h_change oc c cl = - abstract_tactic (TacChange (option_map inj_occ oc,inj_open c,cl)) - (change (option_map Redexpr.out_with_occurrences oc) c cl) + abstract_tactic (TacChange (Option.map inj_occ oc,inj_open c,cl)) + (change (Option.map Redexpr.out_with_occurrences oc) c cl) (* Equivalence relations *) let h_reflexivity = abstract_tactic TacReflexivity intros_reflexivity |