diff options
-rw-r--r-- | CHANGES | 2 | ||||
-rw-r--r-- | doc/refman/RefMan-tac.tex | 4 | ||||
-rw-r--r-- | parsing/g_tactic.ml4 | 9 | ||||
-rw-r--r-- | parsing/pptactic.ml | 4 | ||||
-rw-r--r-- | parsing/q_coqast.ml4 | 2 | ||||
-rw-r--r-- | plugins/interface/depends.ml | 3 | ||||
-rw-r--r-- | plugins/interface/pbp.ml | 4 | ||||
-rw-r--r-- | plugins/interface/showproof.ml | 4 | ||||
-rw-r--r-- | plugins/interface/xlate.ml | 4 | ||||
-rw-r--r-- | proofs/tacexpr.ml | 2 | ||||
-rw-r--r-- | tactics/hiddentac.mli | 2 | ||||
-rw-r--r-- | tactics/tacinterp.ml | 10 | ||||
-rw-r--r-- | tactics/tactics.ml | 5 | ||||
-rw-r--r-- | tactics/tactics.mli | 2 |
14 files changed, 33 insertions, 24 deletions
@@ -29,6 +29,8 @@ Tactics - New variant "subst'" of "subst" that supports JMeq. - New tactic "decide lemma with hyp" for rewriting decidability lemmas when one knows which side is true. +- Tactic "exists" and "eexists" supports iteration using + comma-separated arguments. Tactic Language diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex index d3d1ad918..abc294e8b 100644 --- a/doc/refman/RefMan-tac.tex +++ b/doc/refman/RefMan-tac.tex @@ -1515,6 +1515,10 @@ equivalent to {\tt intros; apply ci}. case of existential quantification $\exists x\cdot P(x)$. Then, it is equivalent to {\tt intros; constructor 1 with \bindinglist}. +\item {\tt exists \nelist{\bindinglist}{,}} + + This iteratively applies {\tt exists {\bindinglist}}. + \item {\tt left}\tacindex{left}\\ {\tt right}\tacindex{right} diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4 index d5d32ce5b..875b9dc07 100644 --- a/parsing/g_tactic.ml4 +++ b/parsing/g_tactic.ml4 @@ -602,10 +602,11 @@ GEXTEND Gram | IDENT "eleft"; bl = with_bindings -> TacLeft (true,bl) | IDENT "right"; bl = with_bindings -> TacRight (false,bl) | IDENT "eright"; bl = with_bindings -> TacRight (true,bl) - | IDENT "split"; bl = with_bindings -> TacSplit (false,false,bl) - | IDENT "esplit"; bl = with_bindings -> TacSplit (true,false,bl) - | "exists"; bl = opt_bindings -> TacSplit (false,true,bl) - | IDENT "eexists"; bl = opt_bindings -> TacSplit (true,true,bl) + | IDENT "split"; bl = with_bindings -> TacSplit (false,false,[bl]) + | IDENT "esplit"; bl = with_bindings -> TacSplit (true,false,[bl]) + | "exists"; bll = LIST1 opt_bindings SEP "," -> TacSplit (false,true,bll) + | IDENT "eexists"; bll = LIST1 opt_bindings SEP "," -> + TacSplit (true,true,bll) | IDENT "constructor"; n = num_or_meta; l = with_bindings -> TacConstructor (false,n,l) | IDENT "econstructor"; n = num_or_meta; l = with_bindings -> diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml index bdd9241e3..bed5e1b28 100644 --- a/parsing/pptactic.ml +++ b/parsing/pptactic.ml @@ -819,8 +819,8 @@ and pr_atom1 = function (* Constructors *) | TacLeft (ev,l) -> hov 1 (str (with_evars ev "left") ++ pr_bindings l) | TacRight (ev,l) -> hov 1 (str (with_evars ev "right") ++ pr_bindings l) - | TacSplit (ev,false,l) -> hov 1 (str (with_evars ev "split") ++ pr_bindings l) - | TacSplit (ev,true,l) -> hov 1 (str (with_evars ev "exists") ++ pr_ex_bindings l) + | TacSplit (ev,false,l) -> hov 1 (str (with_evars ev "split") ++ prlist_with_sep pr_coma pr_bindings l) + | TacSplit (ev,true,l) -> hov 1 (str (with_evars ev "exists") ++ prlist_with_sep pr_coma 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/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4 index 606b652c2..91cb681a5 100644 --- a/parsing/q_coqast.ml4 +++ b/parsing/q_coqast.ml4 @@ -394,7 +394,7 @@ let rec mlexpr_of_atomic_tactic = function <:expr< Tacexpr.TacRight $mlexpr_of_bool ev$ $mlexpr_of_binding_kind l$>> | Tacexpr.TacSplit (ev,b,l) -> <:expr< Tacexpr.TacSplit - ($mlexpr_of_bool ev$,$mlexpr_of_bool b$,$mlexpr_of_binding_kind l$)>> + ($mlexpr_of_bool ev$,$mlexpr_of_bool b$,$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/plugins/interface/depends.ml b/plugins/interface/depends.ml index 9e649a5a2..83c156f7b 100644 --- a/plugins/interface/depends.ml +++ b/plugins/interface/depends.ml @@ -342,8 +342,9 @@ let rec depends_of_gen_tactic_expr depends_of_'constr depends_of_'ind depends_of (* Constructors *) | TacLeft (_,cb) | TacRight (_,cb) - | TacSplit (_, _, cb) + | TacSplit (_, _, [cb]) | TacConstructor (_, _, cb) -> depends_of_'a_bindings depends_of_'constr cb acc + | TacSplit _ -> failwith "TODO" | TacAnyConstructor (_,taco) -> Option.fold_right depends_of_'tac taco acc (* Conversion *) diff --git a/plugins/interface/pbp.ml b/plugins/interface/pbp.ml index 01747aa58..663e4ce92 100644 --- a/plugins/interface/pbp.ml +++ b/plugins/interface/pbp.ml @@ -163,7 +163,7 @@ let make_pbp_atomic_tactic = function | PbpTryAssumption (Some a) -> TacTry (TacAtom (zz, TacExact (make_var a))) | PbpExists x -> - TacAtom (zz, TacSplit (false,true,ImplicitBindings [make_pbp_pattern x])) + TacAtom (zz, TacSplit (false,true,[ImplicitBindings [make_pbp_pattern x]])) | PbpGeneralize (h,args) -> let l = List.map make_pbp_pattern args in TacAtom (zz, TacGeneralize [((true,[]),make_app (make_var h) l),Anonymous]) @@ -178,7 +178,7 @@ let make_pbp_atomic_tactic = function (zz, TacElim (false,(make_var hyp_name,ExplicitBindings bind),None)) | PbpTryClear l -> TacTry (TacAtom (zz, TacClear (false,List.map (fun s -> AI (zz,s)) l))) - | PbpSplit -> TacAtom (zz, TacSplit (false,false,NoBindings));; + | PbpSplit -> TacAtom (zz, TacSplit (false,false,[NoBindings]));; let rec make_pbp_tactic = function | PbpThen tl -> make_then (List.map make_pbp_atomic_tactic tl) diff --git a/plugins/interface/showproof.ml b/plugins/interface/showproof.ml index 2ab62763d..aa11609ae 100644 --- a/plugins/interface/showproof.ml +++ b/plugins/interface/showproof.ml @@ -1183,8 +1183,8 @@ let rec natural_ntree ig ntree = TacIntroPattern _ -> natural_intros ig lh g gs ltree | TacIntroMove _ -> natural_intros ig lh g gs ltree | TacFix (_,n) -> natural_fix ig lh g gs n ltree - | TacSplit (_,_,NoBindings) -> natural_split ig lh g gs ge [] ltree - | TacSplit(_,_,ImplicitBindings l) -> natural_split ig lh g gs ge (List.map snd l) ltree + | TacSplit (_,_,[NoBindings]) -> natural_split ig lh g gs ge [] ltree + | TacSplit(_,_,[ImplicitBindings l]) -> natural_split ig lh g gs ge (List.map snd l) ltree | TacGeneralize l -> natural_generalize ig lh g gs ge l ltree | TacRight _ -> natural_right ig lh g gs ltree | TacLeft _ -> natural_left ig lh g gs ltree diff --git a/plugins/interface/xlate.ml b/plugins/interface/xlate.ml index c27b10c63..4d4eff56f 100644 --- a/plugins/interface/xlate.ml +++ b/plugins/interface/xlate.ml @@ -996,8 +996,8 @@ and xlate_tac = | TacIntroMove _ -> xlate_error "TODO" | TacLeft (false,bindl) -> CT_left (xlate_bindings bindl) | TacRight (false,bindl) -> CT_right (xlate_bindings bindl) - | TacSplit (false,false,bindl) -> CT_split (xlate_bindings bindl) - | TacSplit (false,true,bindl) -> CT_exists (xlate_bindings bindl) + | TacSplit (false,false,[bindl]) -> CT_split (xlate_bindings bindl) + | TacSplit (false,true,[bindl]) -> CT_exists (xlate_bindings bindl) | TacSplit _ | TacRight _ | TacLeft _ -> xlate_error "TODO: esplit, eright, etc" | TacExtend (_,"replace", [c1; c2;cl;tac_opt]) -> diff --git a/proofs/tacexpr.ml b/proofs/tacexpr.ml index 65b330c3d..f53327249 100644 --- a/proofs/tacexpr.ml +++ b/proofs/tacexpr.ml @@ -197,7 +197,7 @@ type ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_atomic_tactic_expr = (* Constructors *) | TacLeft of evars_flag * 'constr bindings | TacRight of evars_flag * 'constr bindings - | TacSplit of evars_flag * split_flag * 'constr bindings + | TacSplit of evars_flag * split_flag * 'constr bindings list | TacAnyConstructor of evars_flag * 'tac option | TacConstructor of evars_flag * int or_metaid * 'constr bindings diff --git a/tactics/hiddentac.mli b/tactics/hiddentac.mli index 6f592108b..e0c267c07 100644 --- a/tactics/hiddentac.mli +++ b/tactics/hiddentac.mli @@ -98,7 +98,7 @@ val h_revert : identifier list -> tactic val h_constructor : evars_flag -> int -> open_constr bindings -> tactic val h_left : evars_flag -> open_constr bindings -> tactic val h_right : evars_flag -> open_constr bindings -> tactic -val h_split : evars_flag -> open_constr bindings -> tactic +val h_split : evars_flag -> open_constr bindings list -> tactic val h_one_constructor : int -> tactic val h_simplest_left : tactic diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 9da5678cf..5df025c1a 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -198,8 +198,8 @@ let _ = "eleft", TacLeft(true,NoBindings); "right", TacRight(false,NoBindings); "eright", TacRight(true,NoBindings); - "split", TacSplit(false,false,NoBindings); - "esplit", TacSplit(true,false,NoBindings); + "split", TacSplit(false,false,[NoBindings]); + "esplit", TacSplit(true,false,[NoBindings]); "constructor", TacAnyConstructor (false,None); "econstructor", TacAnyConstructor (true,None); "reflexivity", TacReflexivity; @@ -777,7 +777,7 @@ let rec intern_atomic lf ist x = (* Constructors *) | TacLeft (ev,bl) -> TacLeft (ev,intern_bindings ist bl) | TacRight (ev,bl) -> TacRight (ev,intern_bindings ist bl) - | TacSplit (ev,b,bl) -> TacSplit (ev,b,intern_bindings ist bl) + | TacSplit (ev,b,bll) -> TacSplit (ev,b,List.map (intern_bindings ist) bll) | TacAnyConstructor (ev,t) -> TacAnyConstructor (ev,Option.map (intern_tactic ist) t) | TacConstructor (ev,n,bl) -> TacConstructor (ev,n,intern_bindings ist bl) @@ -2325,7 +2325,7 @@ and interp_atomic ist gl = function (* Constructors *) | TacLeft (ev,bl) -> h_left ev (interp_bindings ist gl bl) | TacRight (ev,bl) -> h_right ev (interp_bindings ist gl bl) - | TacSplit (ev,_,bl) -> h_split ev (interp_bindings ist gl bl) + | TacSplit (ev,_,bll) -> h_split ev (List.map (interp_bindings ist gl) bll) | TacAnyConstructor (ev,t) -> abstract_tactic (TacAnyConstructor (ev,t)) (Tactics.any_constructor ev (Option.map (interp_tactic ist) t)) @@ -2649,7 +2649,7 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with (* Constructors *) | TacLeft (ev,bl) -> TacLeft (ev,subst_bindings subst bl) | TacRight (ev,bl) -> TacRight (ev,subst_bindings subst bl) - | TacSplit (ev,b,bl) -> TacSplit (ev,b,subst_bindings subst bl) + | TacSplit (ev,b,bll) -> TacSplit (ev,b,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) diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 663c426f9..1ac95f728 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -1166,7 +1166,8 @@ let any_constructor with_evars tacopt gl = let left_with_ebindings with_evars = constructor_tac with_evars (Some 2) 1 let right_with_ebindings with_evars = constructor_tac with_evars (Some 2) 2 -let split_with_ebindings with_evars = constructor_tac with_evars (Some 1) 1 +let split_with_ebindings with_evars = + tclMAP (constructor_tac with_evars (Some 1) 1) let left l = left_with_ebindings false (inj_ebindings l) let simplest_left = left NoBindings @@ -1174,7 +1175,7 @@ let simplest_left = left NoBindings let right l = right_with_ebindings false (inj_ebindings l) let simplest_right = right NoBindings -let split l = split_with_ebindings false (inj_ebindings l) +let split l = split_with_ebindings false [inj_ebindings l] let simplest_split = split NoBindings diff --git a/tactics/tactics.mli b/tactics/tactics.mli index 6e52546f4..ee2250b34 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -324,7 +324,7 @@ val split : constr bindings -> tactic val left_with_ebindings : evars_flag -> open_constr bindings -> tactic val right_with_ebindings : evars_flag -> open_constr bindings -> tactic -val split_with_ebindings : evars_flag -> open_constr bindings -> tactic +val split_with_ebindings : evars_flag -> open_constr bindings list -> tactic val simplest_left : tactic val simplest_right : tactic |