The tactic interpreter now uses a new type of tactics, through

the GTac module. A ['a Gtac.t] is a special case of tactic that
may depend on the current goals, or not. Internally, it construct
a list of results, one for each focussed goal, if the tactic is
actually dependent.

This allows for an interpretation of whole-goal tactic that does
work, which was not the case for the previous implementation,
which did to many Proofview.Goal.enter.

1 files changed, 14 insertions, 0 deletions

diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index 6651e49652..eaaa1f7c30 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -826,6 +826,20 @@ module Goal = struct
         tclZERO e
     end
 
+  let goals =
+    Proof.current >>= fun env ->
+    Proof.get >>= fun step ->
+    let sigma = step.solution in
+    let map goal =
+      match Goal.advance sigma goal with
+      | None -> None (** ppedrot: Is this check really necessary? *)
+      | Some goal ->
+        (** The sigma is unchanged. *)
+        let (gl, _) = Goal.eval (enter_t (fun gl -> gl)) env sigma goal in
+        Some gl
+    in
+    tclUNIT (List.map_filter map step.comb)
+
   (* compatibility *)
   let goal { self=self } = self
   let refresh_sigma g =