Constraining refine to monotonic functions.

2 files changed, 9 insertions, 4 deletions

diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index 11b7d07d05..f549913f2f 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -16,6 +16,7 @@
 open Pp
 open Util
 open Proofview_monad
+open Sigma.Notations
 
 (** Main state of tactics *)
 type proofview = Proofview_monad.proofview
@@ -1031,7 +1032,7 @@ struct
     let prev_future_goals = Evd.future_goals sigma in
     let prev_principal_goal = Evd.principal_future_goal sigma in
     (** Create the refinement term *)
-    let (sigma, c) = f (Evd.reset_future_goals sigma) in
+    let (c, sigma) = Sigma.run (Evd.reset_future_goals sigma) f in
     let evs = Evd.future_goals sigma in
     let evkmain = Evd.principal_future_goal sigma in
     (** Check that the introduced evars are well-typed *)
@@ -1074,7 +1075,11 @@ struct
   let refine_casted ?unsafe f = Goal.enter begin fun gl ->
     let concl = Goal.concl gl in
     let env = Goal.env gl in
-    let f h = let (h, c) = f h in with_type env h c concl 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
+      Sigma (c, Sigma.Unsafe.of_evar_map sigma, p)
+    } in
     refine ?unsafe f
   end
 end
diff --git a/proofs/proofview.mli b/proofs/proofview.mli
index 98e1477ff1..04ca01ec4d 100644
--- a/proofs/proofview.mli
+++ b/proofs/proofview.mli
@@ -487,7 +487,7 @@ module Refine : sig
 
   (** {7 Refinement primitives} *)
 
-  val refine : ?unsafe:bool -> (Evd.evar_map -> Evd.evar_map * Constr.t) -> unit tactic
+  val refine : ?unsafe:bool -> Constr.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
@@ -503,7 +503,7 @@ module Refine : sig
   (** [with_type env sigma c t] ensures that [c] is of type [t]
       inserting a coercion if needed. *)
 
-  val refine_casted : ?unsafe:bool -> (Evd.evar_map -> Evd.evar_map*Constr.t) -> unit tactic
+  val refine_casted : ?unsafe:bool -> Constr.t Sigma.run -> unit tactic
   (** Like {!refine} except the refined term is coerced to the conclusion of the
       current goal. *)