Proofview.Goal primitive now return EConstrs.

1 files changed, 2 insertions, 2 deletions

diff --git a/engine/proofview.mli b/engine/proofview.mli
index 725445251d..2350592a29 100644
--- a/engine/proofview.mli
+++ b/engine/proofview.mli
@@ -484,7 +484,7 @@ 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 -> Term.constr
+  val concl : ([ `NF ], 'r) t -> EConstr.constr
   val hyps : ([ `NF ], 'r) t -> Context.Named.t
   val env : ('a, 'r) t -> Environ.env
   val sigma : ('a, 'r) t -> 'r Sigma.t
@@ -492,7 +492,7 @@ module Goal : sig
 
   (** Returns the goal's conclusion even if the goal is not
       normalised. *)
-  val raw_concl : ('a, 'r) t -> Term.constr
+  val raw_concl : ('a, 'r) t -> EConstr.constr
 
   type ('a, 'b) enter =
     { enter : 'r. ('a, 'r) t -> 'b }