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.mli | 9 --------- 1 file changed, 9 deletions(-) (limited to 'engine/proofview.mli') diff --git a/engine/proofview.mli b/engine/proofview.mli index 1905686fe..970bf6773 100644 --- a/engine/proofview.mli +++ b/engine/proofview.mli @@ -495,10 +495,6 @@ module Goal : sig (** Type of goals. *) type t - (** Assume that you do not need the goal to be normalized. *) - val assume : t -> t - [@@ocaml.deprecated "Normalization is enforced by EConstr, [assume] is not needed anymore"] - (** Normalises the argument goal. *) val normalize : t -> t tactic @@ -589,11 +585,6 @@ module V82 : sig (in chronological order of insertion). *) val grab : proofview -> proofview - (* Returns the open goals of the proofview together with the evar_map to - interpret them. *) - val goals : proofview -> Evar.t list Evd.sigma - [@@ocaml.deprecated "Use [Proofview.proofview]"] - val top_goals : entry -> proofview -> Evar.t list Evd.sigma (* returns the existential variable used to start the proof *) -- cgit v1.2.3