diff options
| author | Cyprien Mangin | 2016-06-03 10:24:36 +0200 |
|---|---|---|
| committer | Cyprien Mangin | 2016-06-14 06:21:31 +0200 |
| commit | 98ed04803e022e66e17f91526ef708484fd17217 (patch) | |
| tree | bc123047c60c6a9fee3a90d832824d6df62bffee /tactics | |
| parent | 9356f42d5f84f9b325f71bab041d1b8184384a21 (diff) | |
Goal selectors are now tacticals and can be used as such.
This allows to write things like this:
split; 2: intro _; exact I
or like this:
eexists ?[x]; ?[x]: exact 0; trivial
This has the side-effect on making the '?' before '[x]' mandatory.
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 |