Do not ask for a normalized goal to get hypotheses and conclusions.

This is now useless as this returns evar-constrs, so that all functions acting
on them should be insensitive to evar-normalization.

1 files changed, 2 insertions, 6 deletions

diff --git a/engine/proofview.mli b/engine/proofview.mli
index 025e3de20..4f662b294 100644
--- a/engine/proofview.mli
+++ b/engine/proofview.mli
@@ -485,16 +485,12 @@ module Goal : sig
       respectively the conclusion of [gl], the hypotheses of [gl], the
       environment of [gl] (i.e. the global environment and the
       hypotheses) and the current evar map. *)
-  val concl : ([ `NF ], 'r) t -> constr
-  val hyps : ([ `NF ], 'r) t -> named_context
+  val concl : ('a, 'r) t -> constr
+  val hyps : ('a, 'r) t -> named_context
   val env : ('a, 'r) t -> Environ.env
   val sigma : ('a, 'r) t -> 'r Sigma.t
   val extra : ('a, 'r) t -> Evd.Store.t
 
-  (** Returns the goal's conclusion even if the goal is not
-      normalised. *)
-  val raw_concl : ('a, 'r) t -> constr
-
   type ('a, 'b) enter =
     { enter : 'r. ('a, 'r) t -> 'b }