From 259ec71685cf2180403e35acea32cb42ba6b761b Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 23 May 2014 18:41:47 +0200
Subject: 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.
---
 proofs/proofview.ml  | 14 ++++++++++++++
 proofs/proofview.mli |  4 ++++
 2 files changed, 18 insertions(+)

(limited to 'proofs')

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 =
diff --git a/proofs/proofview.mli b/proofs/proofview.mli
index 6177803c78..c27e4ba1a9 100644
--- a/proofs/proofview.mli
+++ b/proofs/proofview.mli
@@ -370,8 +370,12 @@ module Goal : sig
      each goal. *)
   val enter : ([ `NF ] t -> unit tactic) -> unit tactic
 
+  (** Same as enter, but does not normalize the goal beforehand. *)
   val raw_enter : ([ `LZ ] t -> unit tactic) -> unit tactic
 
+  (** Recover the list of current goals under focus *)
+  val goals : [ `NF ] t list tactic
+
   (* compatibility: avoid if possible *)
   val goal : [ `NF ] t -> Goal.goal
 
-- 
cgit v1.2.3