aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs
diff options
context:
space:
mode:
authorGravatar Arnaud Spiwack <arnaud@spiwack.net>2014-10-17 16:23:01 +0200
committerGravatar Arnaud Spiwack <arnaud@spiwack.net>2014-10-22 07:31:45 +0200
commitaa64260119704620540017a23815cd7c40c3cff3 (patch)
tree677157e51849510130e868d93193fa8c4b3f1ca2 /proofs
parenta5a355ec3e9cbbfa28be53b9ba6ef914136b0aba (diff)
Proofview: remove a redundant primitive.
Diffstat (limited to 'proofs')
-rw-r--r--proofs/proof.ml11
-rw-r--r--proofs/proofview.ml5
-rw-r--r--proofs/proofview.mli4
3 files changed, 5 insertions, 15 deletions
diff --git a/proofs/proof.ml b/proofs/proof.ml
index d8a7103ec..15ce94011 100644
--- a/proofs/proof.ml
+++ b/proofs/proof.ml
@@ -320,11 +320,10 @@ let run_tactic env tac pr =
let sp = pr.proofview in
let (_,tacticced_proofview,(status,to_shelve,give_up)) = Proofview.apply env tac sp in
let shelf =
- Proofview.in_proofview tacticced_proofview begin fun sigma ->
- let pre_shelf = pr.shelf@(Evd.future_goals sigma)@to_shelve in
- (* avoid already to count already solved goals as shelved. *)
- List.filter (fun g -> Evd.is_undefined sigma g) pre_shelf
- end
+ let sigma = Proofview.return tacticced_proofview in
+ let pre_shelf = pr.shelf@(Evd.future_goals sigma)@to_shelve in
+ (* avoid already to count already solved goals as shelved. *)
+ List.filter (fun g -> Evd.is_undefined sigma g) pre_shelf
in
let given_up = pr.given_up@give_up in
let proofview = Proofview.Unsafe.reset_future_goals tacticced_proofview in
@@ -332,7 +331,7 @@ let run_tactic env tac pr =
(*** Commands ***)
-let in_proof p k = Proofview.in_proofview p.proofview k
+let in_proof p k = k (Proofview.return p.proofview)
(* Remove all the goals from the shelf and adds them at the end of the
focused goals. *)
diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index a84a2d34d..98a6e7c14 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -849,11 +849,6 @@ let numgoals =
Pv.get >>= fun { comb } ->
Proof.ret (List.length comb)
-(*** Commands ***)
-
-let in_proofview p k =
- k p.solution
-
module Unsafe = struct
(* A [Proofview.tactic] version of [Refiner.tclEVARS] *)
diff --git a/proofs/proofview.mli b/proofs/proofview.mli
index b8179f4fa..0d9c64a5c 100644
--- a/proofs/proofview.mli
+++ b/proofs/proofview.mli
@@ -326,10 +326,6 @@ end
module Monad : Monad.S with type +'a t = 'a tactic
-(*** Commands ***)
-
-val in_proofview : proofview -> (Evd.evar_map -> 'a) -> 'a
-
(* Notations for building tactics. *)
module Notations : sig