3 files changed, 32 insertions, 4 deletions
diff --git a/engine/ftactic.ml b/engine/ftactic.ml
index 588709873e..aeaaea7e48 100644
--- a/engine/ftactic.ml
+++ b/engine/ftactic.ml
@@ -29,13 +29,28 @@ let bind (type a) (type b) (m : a t) (f : a -> b t) : b t = m >>= function
   | Uniform x ->
     (** We dispatch the uniform result on each goal under focus, as we know
         that the [m] argument was actually dependent. *)
-    Proofview.Goal.goals >>= fun l ->
-    let ans = List.map (fun _ -> x) l in
+    Proofview.Goal.goals >>= fun goals ->
+    let ans = List.map (fun g -> (g,x)) goals in
     Proofview.tclUNIT ans
-  | Depends l -> Proofview.tclUNIT l
+  | Depends l ->
+    Proofview.Goal.goals >>= fun goals ->
+    Proofview.tclUNIT (List.combine goals l)
+  in
+  (* After the tactic has run, some goals which were previously
+     produced may have been solved by side effects. The values
+     attached to such goals must be discarded, otherwise the list of
+     result would not have the same length as the list of focused
+     goals, which is an invariant of the [Ftactic] module. It is the
+     reason why a goal is attached to each result above. *)
+  let filter (g,x) =
+    g >>= fun g ->
+    Proofview.Goal.unsolved g >>= function
+    | true -> Proofview.tclUNIT (Some x)
+    | false -> Proofview.tclUNIT None
   in
   Proofview.tclDISPATCHL (List.map f l) >>= fun l ->
-  Proofview.tclUNIT (Depends (List.concat l))
+  Proofview.Monad.List.map_filter filter (List.concat l) >>= fun filtered ->
+  Proofview.tclUNIT (Depends filtered)
 
 let goals = Proofview.Goal.goals >>= fun l -> Proofview.tclUNIT (Depends l)
 let set_sigma r =
diff --git a/engine/proofview.ml b/engine/proofview.ml
index a2838a2de1..f2f4005151 100644
--- a/engine/proofview.ml
+++ b/engine/proofview.ml
@@ -929,6 +929,8 @@ module Unsafe = struct
       { step with comb = step.comb @ gls }
     end
 
+  let tclSETENV = Env.set
+
   let tclGETGOALS = Comb.get
 
   let tclSETGOALS = Comb.set
@@ -1129,6 +1131,10 @@ module Goal = struct
     in
     tclUNIT (CList.map_filter map step.comb)
 
+  let unsolved { self=self } =
+    tclEVARMAP >>= fun sigma ->
+    tclUNIT (not (Option.is_empty (advance sigma self)))
+
   (* compatibility *)
   let goal { self=self } = self
 
diff --git a/engine/proofview.mli b/engine/proofview.mli
index bc68f11ff0..fae75f8254 100644
--- a/engine/proofview.mli
+++ b/engine/proofview.mli
@@ -409,6 +409,9 @@ module Unsafe : sig
   (** Like {!tclEVARS} but also checks whether goals have been solved. *)
   val tclEVARSADVANCE : Evd.evar_map -> unit tactic
 
+  (** Set the global environment of the tactic *)
+  val tclSETENV : Environ.env -> unit tactic
+
   (** [tclNEWGOALS gls] adds the goals [gls] to the ones currently
       being proved, appending them to the list of focused goals. If a
       goal is already solved, it is not added. *)
@@ -518,6 +521,10 @@ module Goal : sig
       FIXME: encapsulate the level in an existential type. *)
   val goals : ([ `LZ ], 'r) t tactic list tactic
 
+  (** [unsolved g] is [true] if [g] is still unsolved in the current
+      proof state. *)
+  val unsolved : ('a, 'r) t -> bool tactic
+
   (** Compatibility: avoid if possible *)
   val goal : ([ `NF ], 'r) t -> Evar.t