diff options
| author |  aspiwack <aspiwack@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-11-04 18:08:46 +0000 |
|---|---|---|
| committer | aspiwack <aspiwack@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-11-04 18:08:46 +0000 |
| commit | 5f4a61935e048a8e4490f5610e551d8844a373c4 (patch) | |
| tree | 7a53bac5bdb769224b4b7057940573770e450eb3 /tactics/tacticals.mli | |
| parent | e3d3d73dfca0576cb25ce555cc445c657baecb19 (diff) | |
Fix ltac's progress tactical: requires progress in each goal.
Proofview.tclPROGRESS considers that a tactic that changes the list of goal progresses, under this semantics, "progress auto" succeeds if its applied to two goals and solves the first one but not the second one. This would break backwards compatibility.
Spotted in Fermat4.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17058 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics/tacticals.mli')
| -rw-r--r-- | tactics/tacticals.mli | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli index 312e5cb49..f1e8a3403 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 |