From 0dc79e09b2b7c369b35191191aa257451a536540 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sun, 11 Mar 2018 01:14:28 +0100 Subject: [api] Remove deprecated objects in engine / interp / library --- engine/proofview.ml | 7 ------- 1 file changed, 7 deletions(-) (limited to 'engine/proofview.ml') 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; } -- cgit v1.2.3