Chasing the goal entering backward while interpreting tactics. This required

writing a new primitive recovering the first goal under focus. It sounds a bit
hackish, but it does actually work.

2 files changed, 19 insertions, 2 deletions

diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index 6651e49652..b32b1d62db 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -826,6 +826,21 @@ module Goal = struct
         tclZERO e
     end
 
+  let goals =
+    let (>>=) = Proof.bind in
+    Proof.current >>= fun env ->
+    Proof.get >>= fun step ->
+    let map goal =
+      let goal = Goal.advance step.solution goal in
+      match goal with
+      | None -> None
+      | Some g ->
+        let (t, _) = Goal.eval (enter_t (fun x -> x)) env step.solution g in
+        Some t
+    in
+    let goals = List.map_filter map step.comb in
+    Proof.ret goals
+
   (* compatibility *)
   let goal { self=self } = self
   let refresh_sigma g =
@@ -861,5 +876,4 @@ end
 module NonLogical = Proofview_monad.NonLogical
 
 let tclLIFT = Proofview_monad.Logical.lift
-
-
+let tclGOALS = Goal.goals
diff --git a/proofs/proofview.mli b/proofs/proofview.mli
index 6177803c78..769bfb001f 100644
--- a/proofs/proofview.mli
+++ b/proofs/proofview.mli
@@ -453,3 +453,6 @@ end
 
 (* [tclLIFT c] includes the non-logical command [c] in a tactic. *)
 val tclLIFT : 'a NonLogical.t -> 'a tactic
+
+(* Access the current goals *)
+val tclGOALS : [ `NF ] Goal.t list tactic