diff options
| -rw-r--r-- | doc/refman/RefMan-ltac.tex | 3 | ||||
| -rw-r--r-- | tactics/tacinterp.ml | 2 | ||||
| -rw-r--r-- | tactics/tacticals.ml | 2 | ||||
| -rw-r--r-- | tactics/tacticals.mli | 1 |
4 files changed, 6 insertions, 2 deletions
diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex index ae5653c145..13b2d387b8 100644 --- a/doc/refman/RefMan-ltac.tex +++ b/doc/refman/RefMan-ltac.tex @@ -371,7 +371,8 @@ We can check if a tactic made progress with: {\tt progress} {\tacexpr} \end{quote} {\tacexpr} is evaluated to $v$. $v$ must be a tactic value. $v$ is -applied. If the application of $v$ produced subgoals equal to the +applied to each focued subgoal independently. If the application of +$v$ to one of the focused subgoal produced subgoals equal to the initial goals (up to syntactical equality), then an error of level 0 is raised. diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index c19159eeea..34314088c0 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -1131,7 +1131,7 @@ and eval_tactic ist = function Proofview.V82.tactic begin fun gl -> tclFAIL (interp_int_or_var ist n) (interp_message ist gl s) gl end - | TacProgress tac -> Proofview.tclPROGRESS (interp_tactic ist tac) + | TacProgress tac -> Tacticals.New.tclPROGRESS (interp_tactic ist tac) | TacShowHyps tac -> Proofview.V82.tactic begin tclSHOWHYPS (Proofview.V82.of_tactic (interp_tactic ist tac)) diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index bcb6041eff..f815830ca2 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -510,6 +510,8 @@ module New = struct (* Try the first thats solves the current goal *) let tclSOLVE tacl = tclFIRST (List.map tclCOMPLETE tacl) + let tclPROGRESS t = + Proofview.tclINDEPENDENT (Proofview.tclPROGRESS t) let tclWITHHOLES accept_unresolved_holes tac sigma x = tclEVARMAP >= fun sigma_initial -> diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli index 312e5cb494..f1e8a34033 100644 --- a/tactics/tacticals.mli +++ b/tactics/tacticals.mli @@ -236,6 +236,7 @@ module New : sig val tclREPEAT_MAIN : unit tactic -> unit tactic val tclCOMPLETE : 'a tactic -> 'a tactic val tclSOLVE : unit tactic list -> unit tactic + val tclPROGRESS : unit tactic -> unit tactic val tclWITHHOLES : bool -> ('a -> unit tactic) -> Evd.evar_map -> 'a -> unit tactic val tclTIMEOUT : int -> unit tactic -> unit tactic |