diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/tacticals.ml | 7 | ||||
| -rw-r--r-- | tactics/tacticals.mli | 1 |
2 files changed, 8 insertions, 0 deletions
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index 7f904a561d..3d51623eaa 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -476,6 +476,13 @@ module New = struct let tclPROGRESS t = Proofview.tclINDEPENDENT (Proofview.tclPROGRESS t) + (* Select a subset of the goals *) + let tclSELECT = function + | Tacexpr.SelectNth i -> Proofview.tclFOCUS i i + | Tacexpr.SelectList l -> Proofview.tclFOCUSLIST l + | Tacexpr.SelectId id -> Proofview.tclFOCUSID id + | Tacexpr.SelectAll -> fun tac -> tac + (* Check that holes in arguments have been resolved *) let check_evars env sigma extsigma origsigma = diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli index 0f926468b9..cfdc2cffd4 100644 --- a/tactics/tacticals.mli +++ b/tactics/tacticals.mli @@ -221,6 +221,7 @@ module New : sig val tclCOMPLETE : 'a tactic -> 'a tactic val tclSOLVE : unit tactic list -> unit tactic val tclPROGRESS : unit tactic -> unit tactic + val tclSELECT : goal_selector -> 'a tactic -> 'a tactic val tclWITHHOLES : bool -> 'a tactic -> Evd.evar_map -> 'a tactic val tclDELAYEDWITHHOLES : bool -> 'a delayed_open -> ('a -> unit tactic) -> unit tactic |