aboutsummaryrefslogtreecommitdiffhomepage
path: root/engine/proofview.ml
diff options
context:
space:
mode:
authorGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2018-03-11 01:14:28 +0100
committerGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2018-05-30 17:50:37 +0200
commit0dc79e09b2b7c369b35191191aa257451a536540 (patch)
tree56ecf715bf703828818c31a2279718cc1e31d479 /engine/proofview.ml
parent118d24281bc62bb7ff503abee56f156545eb9eea (diff)
[api] Remove deprecated objects in engine / interp / library
Diffstat (limited to 'engine/proofview.ml')
-rw-r--r--engine/proofview.ml7
1 files changed, 0 insertions, 7 deletions
diff --git a/engine/proofview.ml b/engine/proofview.ml
index 54237ceb4..fdb0a215d 100644
--- a/engine/proofview.ml
+++ b/engine/proofview.ml
@@ -1085,8 +1085,6 @@ module Goal = struct
self : Evar.t ; (* for compatibility with old-style definitions *)
}
- let assume (gl : t) = (gl : t)
-
let print { sigma; self } = { Evd.it = self; sigma }
let state { state=state } = state
@@ -1274,11 +1272,6 @@ module V82 = struct
- (* Returns the open goals of the proofview together with the evar_map to
- interpret them. *)
- let goals { comb = comb ; solution = solution; } =
- { Evd.it = List.map drop_state comb ; sigma = solution }
-
let top_goals initial { solution=solution; } =
let goals = CList.map (fun (t,_) -> fst (Constr.destEvar (EConstr.Unsafe.to_constr t))) initial in
{ Evd.it = goals ; sigma=solution; }