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

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