Goal API using EConstr.

1 files changed, 6 insertions, 2 deletions

diff --git a/proofs/goal.ml b/proofs/goal.ml
index bcb14e2d6..4c598ca29 100644
--- a/proofs/goal.ml
+++ b/proofs/goal.ml
@@ -62,6 +62,7 @@ module V82 = struct
        be shelved. It must not appear as a future_goal, so the future
        goals are restored to their initial value after the evar is
        created. *)
+    let concl = EConstr.Unsafe.to_constr concl in
     let prev_future_goals = Evd.future_goals evars in
     let prev_principal_goal = Evd.principal_future_goal evars in
     let evi = { Evd.evar_hyps = hyps;
@@ -78,13 +79,14 @@ module V82 = struct
     let evars = Sigma.to_evar_map evars in
     let evars = Evd.restore_future_goals evars prev_future_goals prev_principal_goal in
     let ctxt = Environ.named_context_of_val hyps in
-    let inst = Array.map_of_list (NamedDecl.get_id %> mkVar) ctxt in
-    let ev = Term.mkEvar (evk,inst) in
+    let inst = Array.map_of_list (NamedDecl.get_id %> EConstr.mkVar) ctxt in
+    let ev = EConstr.mkEvar (evk,inst) in
     (evk, ev, evars)
 
   (* Instantiates a goal with an open term *)
   let partial_solution sigma evk c =
     (* Check that the goal itself does not appear in the refined term *)
+    let c = EConstr.Unsafe.to_constr c in
     let _ =
       if not (Evarutil.occur_evar_upto sigma evk c) then ()
       else Pretype_errors.error_occur_check Environ.empty_env sigma evk (EConstr.of_constr c)
@@ -158,4 +160,6 @@ module V82 = struct
 					    t
 				       ) ~init:(concl sigma gl) env
 
+  let concl sigma gl = EConstr.of_constr (concl sigma gl)
+
 end