diff options
Diffstat (limited to 'engine/proofview.mli')
| -rw-r--r-- | engine/proofview.mli | 9 |
1 files changed, 0 insertions, 9 deletions
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 *) |