From 1f0284e591c7315149509200239fc9c821c2c9dd Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sat, 24 May 2014 15:31:48 +0200
Subject: Revert "Chasing the goal entering backward while interpreting
 tactics. This required" I tested the commit on the wrong branch...

This reverts commit b0364eff4ec8ad5676060d8ca9cdbbb1d9c34d04.
---
 proofs/proofview.ml  | 18 ++----------------
 proofs/proofview.mli |  3 ---
 2 files changed, 2 insertions(+), 19 deletions(-)

(limited to 'proofs')

diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index b32b1d62db..6651e49652 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -826,21 +826,6 @@ 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 =
@@ -876,4 +861,5 @@ 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 769bfb001f..6177803c78 100644
--- a/proofs/proofview.mli
+++ b/proofs/proofview.mli
@@ -453,6 +453,3 @@ 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
-- 
cgit v1.2.3