3 files changed, 9 insertions, 4 deletions
diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index 2d621e97cb..956be88c8a 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -669,12 +669,14 @@ let evar_of_binder holes = function
     user_err  (str "No such binder.")
 
 let define_with_type sigma env ev c =
+  let c = EConstr.of_constr c in
   let t = Retyping.get_type_of env sigma (EConstr.of_constr ev) in
-  let ty = Retyping.get_type_of env sigma (EConstr.of_constr c) in
+  let ty = Retyping.get_type_of env sigma c in
+  let ty = EConstr.of_constr ty in
   let j = Environ.make_judge c ty in
   let (sigma, j) = Coercion.inh_conv_coerce_to true (Loc.ghost) env sigma j (EConstr.of_constr t) in
   let (ev, _) = destEvar ev in
-  let sigma = Evd.define ev j.Environ.uj_val sigma in
+  let sigma = Evd.define ev (EConstr.Unsafe.to_constr j.Environ.uj_val) sigma in
   sigma
 
 let solve_evar_clause env sigma hyp_only clause = function
diff --git a/proofs/refine.ml b/proofs/refine.ml
index 0ed74c9b36..067764c000 100644
--- a/proofs/refine.ml
+++ b/proofs/refine.ml
@@ -133,7 +133,9 @@ let refine ?(unsafe = true) f =
 (** Useful definitions *)
 
 let with_type env evd c t =
-  let my_type = Retyping.get_type_of env evd (EConstr.of_constr c) in
+  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)
@@ -147,6 +149,7 @@ let refine_casted ?unsafe f = Proofview.Goal.enter { enter = begin fun gl ->
   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 3d140f036b..4158e446cc 100644
--- a/proofs/refine.mli
+++ b/proofs/refine.mli
@@ -36,7 +36,7 @@ val refine_one : ?unsafe:bool -> ('a * Constr.t) Sigma.run -> 'a tactic
 (** {7 Helper functions} *)
 
 val with_type : Environ.env -> Evd.evar_map ->
-  Term.constr -> Term.types -> Evd.evar_map * Term.constr
+  Term.constr -> Term.types -> Evd.evar_map * EConstr.constr
 (** [with_type env sigma c t] ensures that [c] is of type [t]
     inserting a coercion if needed. *)