diff options
| author | Pierre-Marie Pédrot | 2014-05-24 15:31:48 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2014-05-24 15:35:08 +0200 |
| commit | 1f0284e591c7315149509200239fc9c821c2c9dd (patch) | |
| tree | fe101b5f3b52211e8da8fd75765f44170d7632c6 /proofs | |
| parent | b0364eff4ec8ad5676060d8ca9cdbbb1d9c34d04 (diff) | |
Revert "Chasing the goal entering backward while interpreting tactics. This required"
I tested the commit on the wrong branch...
This reverts commit b0364eff4ec8ad5676060d8ca9cdbbb1d9c34d04.
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/proofview.ml | 18 | ||||
| -rw-r--r-- | proofs/proofview.mli | 3 |
2 files changed, 2 insertions, 19 deletions
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 |