2 files changed, 3 insertions, 4 deletions
diff --git a/proofs/goal.ml b/proofs/goal.ml
index 7499bc251b..410e738de7 100644
--- a/proofs/goal.ml
+++ b/proofs/goal.ml
@@ -49,7 +49,7 @@ module V82 = struct
   (* Access to ".evar_concl" *)
   let concl evars gl =
     let evi = Evd.find evars gl in
-    evi.Evd.evar_concl
+    EConstr.of_constr evi.Evd.evar_concl
 
   (* Access to ".evar_extra" *)
   let extra evars gl =
@@ -146,6 +146,7 @@ module V82 = struct
 
   (* Goal represented as a type, doesn't take into account section variables *)
   let abstract_type sigma gl =
+    let open EConstr in
     let (gl,sigma) = nf_evar sigma gl in
     let env = env sigma gl in
     let genv = Global.env () in
@@ -159,6 +160,4 @@ module V82 = struct
 					    t
 				       ) ~init:(concl sigma gl) env
 
-  let concl sigma gl = EConstr.of_constr (concl sigma gl)
-
 end
diff --git a/proofs/goal.mli b/proofs/goal.mli
index ca6584e76d..a2fa34c05e 100644
--- a/proofs/goal.mli
+++ b/proofs/goal.mli
@@ -75,6 +75,6 @@ module V82 : sig
   val nf_evar : Evd.evar_map -> goal -> goal * Evd.evar_map
 
   (* Goal represented as a type, doesn't take into account section variables *)
-  val abstract_type : Evd.evar_map -> goal -> Term.types 
+  val abstract_type : Evd.evar_map -> goal -> EConstr.types 
 
 end