diff options
| -rw-r--r-- | grammar/q_coqast.ml4 | 4 | ||||
| -rw-r--r-- | intf/tacexpr.mli | 3 | ||||
| -rw-r--r-- | parsing/g_tactic.ml4 | 6 | ||||
| -rw-r--r-- | printing/pptactic.ml | 3 | ||||
| -rw-r--r-- | tactics/coretactics.ml4 | 24 | ||||
| -rw-r--r-- | tactics/tacenv.ml | 2 | ||||
| -rw-r--r-- | tactics/tacintern.ml | 2 | ||||
| -rw-r--r-- | tactics/tacinterp.ml | 2 | ||||
| -rw-r--r-- | tactics/tacsubst.ml | 2 |
9 files changed, 33 insertions, 15 deletions
diff --git a/grammar/q_coqast.ml4 b/grammar/q_coqast.ml4 index cada607f6..528678d1d 100644 --- a/grammar/q_coqast.ml4 +++ b/grammar/q_coqast.ml4 @@ -385,9 +385,9 @@ let rec mlexpr_of_atomic_tactic = function $mlexpr_of_move_location mlexpr_of_hyp id2$ >> (* Constructors *) - | Tacexpr.TacSplit (ev,b,l) -> + | Tacexpr.TacSplit (ev,l) -> <:expr< Tacexpr.TacSplit - ($mlexpr_of_bool ev$,$mlexpr_of_bool b$,$mlexpr_of_list mlexpr_of_binding_kind l$)>> + ($mlexpr_of_bool ev$, $mlexpr_of_list mlexpr_of_binding_kind l$)>> | Tacexpr.TacAnyConstructor (ev,t) -> <:expr< Tacexpr.TacAnyConstructor $mlexpr_of_bool ev$ $mlexpr_of_option mlexpr_of_tactic t$>> | Tacexpr.TacConstructor (ev,n,l) -> diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli index eeba560d7..4b4a54a03 100644 --- a/intf/tacexpr.mli +++ b/intf/tacexpr.mli @@ -26,7 +26,6 @@ type lazy_flag = bool (* true = lazy false = eager *) type evars_flag = bool (* true = pose evars false = fail on evars *) type rec_flag = bool (* true = recursive false = not recursive *) type advanced_flag = bool (* true = advanced false = basic *) -type split_flag = bool (* true = exists false = split *) type letin_flag = bool (* true = use local def false = use Leibniz *) type debug = Debug | Info | Off (* for trivial / auto / eauto ... *) @@ -141,7 +140,7 @@ type ('trm,'pat,'cst,'ind,'ref,'nam,'lev) gen_atomic_tactic_expr = | TacRevert of 'nam list (* Trmuctors *) - | TacSplit of evars_flag * split_flag * 'trm bindings list + | TacSplit of evars_flag * 'trm bindings list | TacAnyConstructor of evars_flag * ('trm,'pat,'cst,'ind,'ref,'nam,'lev) gen_tactic_expr option | TacConstructor of evars_flag * int or_var * 'trm bindings diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4 index a97b73da7..77461213b 100644 --- a/parsing/g_tactic.ml4 +++ b/parsing/g_tactic.ml4 @@ -626,11 +626,9 @@ GEXTEND Gram | IDENT "revert"; l = LIST1 id_or_meta -> TacRevert l (* Constructors *) - | IDENT "split"; bl = with_bindings -> TacSplit (false,false,[bl]) - | IDENT "esplit"; bl = with_bindings -> TacSplit (true,false,[bl]) - | "exists"; bll = opt_bindings -> TacSplit (false,true,bll) + | "exists"; bll = opt_bindings -> TacSplit (false,bll) | IDENT "eexists"; bll = opt_bindings -> - TacSplit (true,true,bll) + TacSplit (true,bll) | IDENT "constructor"; n = nat_or_var; l = with_bindings -> TacConstructor (false,n,l) | IDENT "econstructor"; n = nat_or_var; l = with_bindings -> diff --git a/printing/pptactic.ml b/printing/pptactic.ml index 6c2c67c35..f6c25d069 100644 --- a/printing/pptactic.ml +++ b/printing/pptactic.ml @@ -758,8 +758,7 @@ and pr_atom1 = function hov 1 (str "revert" ++ spc () ++ prlist_with_sep spc pr_ident l) (* Constructors *) - | TacSplit (ev,false,l) -> hov 1 (str (with_evars ev "split") ++ prlist_with_sep pr_comma pr_bindings l) - | TacSplit (ev,true,l) -> hov 1 (str (with_evars ev "exists") ++ prlist_with_sep (fun () -> str",") pr_ex_bindings l) + | TacSplit (ev,l) -> hov 1 (str (with_evars ev "exists") ++ prlist_with_sep (fun () -> str",") pr_ex_bindings l) | TacAnyConstructor (ev,Some t) -> hov 1 (str (with_evars ev "constructor") ++ pr_arg (pr_tac_level (latom,E)) t) | TacAnyConstructor (ev,None) as t -> pr_atom0 t diff --git a/tactics/coretactics.ml4 b/tactics/coretactics.ml4 index 283cff73f..a95d71443 100644 --- a/tactics/coretactics.ml4 +++ b/tactics/coretactics.ml4 @@ -118,3 +118,27 @@ END TACTIC EXTEND symmetry [ "symmetry" ] -> [ Tactics.intros_symmetry {onhyps=Some[];concl_occs=AllOccurrences} ] END + +(** Split *) + +TACTIC EXTEND split + [ "split" ] -> [ Tactics.split_with_bindings false [NoBindings] ] +END + +TACTIC EXTEND esplit + [ "esplit" ] -> [ Tactics.split_with_bindings true [NoBindings] ] +END + +TACTIC EXTEND split_with + [ "split" "with" bindings(bl) ] -> [ + let { Evd.sigma = sigma ; it = bl } = bl in + Tacticals.New.tclWITHHOLES false (Tactics.split_with_bindings false) sigma [bl] + ] +END + +TACTIC EXTEND esplit_with + [ "esplit" "with" bindings(bl) ] -> [ + let { Evd.sigma = sigma ; it = bl } = bl in + Tacticals.New.tclWITHHOLES true (Tactics.split_with_bindings true) sigma [bl] + ] +END diff --git a/tactics/tacenv.ml b/tactics/tacenv.ml index 9da5d44e0..5ce914a9c 100644 --- a/tactics/tacenv.ml +++ b/tactics/tacenv.ml @@ -80,8 +80,6 @@ let initial_atomic = "cofix", TacCofix None; "trivial", TacTrivial (Off,[],None); "auto", TacAuto(Off,None,[],None); - "split", TacSplit(false,false,[NoBindings]); - "esplit", TacSplit(true,false,[NoBindings]); "constructor", TacAnyConstructor (false,None); "econstructor", TacAnyConstructor (true,None); ] diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml index 4d711af9a..35952c9dd 100644 --- a/tactics/tacintern.ml +++ b/tactics/tacintern.ml @@ -520,7 +520,7 @@ let rec intern_atomic lf ist x = | TacRevert l -> TacRevert (List.map (intern_hyp_or_metaid ist) l) (* Constructors *) - | TacSplit (ev,b,bll) -> TacSplit (ev,b,List.map (intern_bindings ist) bll) + | TacSplit (ev,bll) -> TacSplit (ev,List.map (intern_bindings ist) bll) | TacAnyConstructor (ev,t) -> TacAnyConstructor (ev,Option.map (intern_pure_tactic ist) t) | TacConstructor (ev,n,bl) -> TacConstructor (ev,intern_or_var ist n,intern_bindings ist bl) diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 9ca9aabab..1ca63b53a 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -1690,7 +1690,7 @@ and interp_atomic ist tac : unit Proofview.tactic = end (* Constructors *) - | TacSplit (ev,_,bll) -> + | TacSplit (ev,bll) -> Proofview.Goal.raw_enter begin fun gl -> let env = Proofview.Goal.env gl in let sigma = Proofview.Goal.sigma gl in diff --git a/tactics/tacsubst.ml b/tactics/tacsubst.ml index 622245524..aa090b715 100644 --- a/tactics/tacsubst.ml +++ b/tactics/tacsubst.ml @@ -178,7 +178,7 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with | TacRevert _ as x -> x (* Constructors *) - | TacSplit (ev,b,bll) -> TacSplit (ev,b,List.map (subst_bindings subst) bll) + | TacSplit (ev,bll) -> TacSplit (ev,List.map (subst_bindings subst) bll) | TacAnyConstructor (ev,t) -> TacAnyConstructor (ev,Option.map (subst_tactic subst) t) | TacConstructor (ev,n,bl) -> TacConstructor (ev,n,subst_bindings subst bl) |