Refine API using EConstr.

3 files changed, 12 insertions, 12 deletions

diff --git a/proofs/goal.ml b/proofs/goal.ml
index 4c598ca29e..7499bc251b 100644
--- a/proofs/goal.ml
+++ b/proofs/goal.ml
@@ -86,12 +86,11 @@ module V82 = struct
   (* 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)
+      else Pretype_errors.error_occur_check Environ.empty_env sigma evk c
     in
-    Evd.define evk c sigma
+    Evd.define evk (EConstr.Unsafe.to_constr c) sigma
 
   (* Instantiates a goal with an open term, using name of goal for evk' *)
   let partial_solution_to sigma evk evk' c =
diff --git a/proofs/refine.ml b/proofs/refine.ml
index 067764c000..11eabe0a90 100644
--- a/proofs/refine.ml
+++ b/proofs/refine.ml
@@ -47,7 +47,7 @@ let typecheck_evar ev env sigma =
 
 let typecheck_proof c concl env sigma =
   let evdref = ref sigma in
-  let () = Typing.e_check env evdref (EConstr.of_constr c) (EConstr.of_constr concl) in
+  let () = Typing.e_check env evdref c concl in
   !evdref
 
 let (pr_constrv,pr_constr) =
@@ -77,6 +77,7 @@ let make_refine_enter ?(unsafe = true) f =
   let sigma = Sigma.to_evar_map sigma in
   let env = Proofview.Goal.env gl in
   let concl = Proofview.Goal.concl gl in
+  let concl = EConstr.of_constr concl in
   (** Save the [future_goals] state to restore them after the
       refinement. *)
   let prev_future_goals = Evd.future_goals sigma in
@@ -98,9 +99,10 @@ let make_refine_enter ?(unsafe = true) f =
   let self = Proofview.Goal.goal gl in
   let _ =
     if not (Evarutil.occur_evar_upto sigma self c) then ()
-    else Pretype_errors.error_occur_check env sigma self (EConstr.of_constr c)
+    else Pretype_errors.error_occur_check env sigma self c
   in
   (** Proceed to the refinement *)
+  let c = EConstr.Unsafe.to_constr c in
   let sigma = match evkmain with
     | None -> Evd.define self c sigma
     | Some evk ->
@@ -133,23 +135,22 @@ let refine ?(unsafe = true) f =
 (** Useful definitions *)
 
 let with_type env evd c t =
-  let c = EConstr.of_constr c in
   let my_type = Retyping.get_type_of env evd c in
   let my_type = EConstr.of_constr my_type in
   let j = Environ.make_judge c my_type in
   let (evd,j') =
-    Coercion.inh_conv_coerce_to true (Loc.ghost) env evd j (EConstr.of_constr t)
+    Coercion.inh_conv_coerce_to true (Loc.ghost) env evd j t
   in
   evd , j'.Environ.uj_val
 
 let refine_casted ?unsafe f = Proofview.Goal.enter { enter = begin fun gl ->
   let gl = Proofview.Goal.assume gl in
   let concl = Proofview.Goal.concl gl in
+  let concl = EConstr.of_constr concl in
   let env = Proofview.Goal.env gl in
   let f = { run = fun h ->
     let Sigma (c, h, p) = f.run h in
     let sigma, c = with_type env (Sigma.to_evar_map h) c concl in
-    let c = EConstr.Unsafe.to_constr c in
     Sigma (c, Sigma.Unsafe.of_evar_map sigma, p)
   } in
   refine ?unsafe f
diff --git a/proofs/refine.mli b/proofs/refine.mli
index 4158e446cc..205b979747 100644
--- a/proofs/refine.mli
+++ b/proofs/refine.mli
@@ -21,7 +21,7 @@ val pr_constr :
 
 (** {7 Refinement primitives} *)
 
-val refine : ?unsafe:bool -> Constr.t Sigma.run -> unit tactic
+val refine : ?unsafe:bool -> EConstr.t Sigma.run -> unit tactic
 (** In [refine ?unsafe t], [t] is a term with holes under some
     [evar_map] context. The term [t] is used as a partial solution
     for the current goal (refine is a goal-dependent tactic), the
@@ -30,16 +30,16 @@ val refine : ?unsafe:bool -> Constr.t Sigma.run -> unit tactic
     tactic failures. If [unsafe] is [false] (default is [true]) [t] is
     type-checked beforehand. *)
 
-val refine_one : ?unsafe:bool -> ('a * Constr.t) Sigma.run -> 'a tactic
+val refine_one : ?unsafe:bool -> ('a * EConstr.t) Sigma.run -> 'a tactic
 (** A generalization of [refine] which assumes exactly one goal under focus *)
 
 (** {7 Helper functions} *)
 
 val with_type : Environ.env -> Evd.evar_map ->
-  Term.constr -> Term.types -> Evd.evar_map * EConstr.constr
+  EConstr.constr -> EConstr.types -> Evd.evar_map * EConstr.constr
 (** [with_type env sigma c t] ensures that [c] is of type [t]
     inserting a coercion if needed. *)
 
-val refine_casted : ?unsafe:bool -> Constr.t Sigma.run -> unit tactic
+val refine_casted : ?unsafe:bool -> EConstr.t Sigma.run -> unit tactic
 (** Like {!refine} except the refined term is coerced to the conclusion of the
     current goal. *)