A handful of useful primitives in Proofview.Refine.

2 files changed, 34 insertions, 3 deletions

diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index 52d8b7d7c..e96e19015 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -910,19 +910,39 @@ struct
     let h = (evd, build_goal evk :: evs) in
     (h, ev)
 
+  let fresh_constructor_instance (evd,evs) env construct =
+    let (evd,pconstruct) = Evd.fresh_constructor_instance env evd construct in
+    (evd,evs) , pconstruct
+
+  let with_type (evd,evs) env c t =
+    let my_type = Retyping.get_type_of env evd c in
+    let j = Environ.make_judge c my_type in
+    let (evd,j') =
+      Coercion.inh_conv_coerce_to true (Loc.ghost) env evd j t
+    in
+    (evd,evs) , j'.Environ.uj_val
+
   let refine f = Goal.raw_enter begin fun gl ->
     let sigma = Goal.sigma gl in
     let handle = (sigma, []) in
     let ((sigma, evs), c) = f handle in
     let sigma = partial_solution sigma gl.Goal.self c in
-    let modify start = { solution = sigma; comb = List.rev evs; } in
+    let modify start = { solution = sigma; comb = undefined sigma (List.rev evs); } in
     Proof.modify modify
   end
 
+  let refine_casted f = Goal.raw_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 h env c concl
+    in
+    refine f
+  end
+
 end
 
 module NonLogical = Proofview_monad.NonLogical
 
 let tclLIFT = Proofview_monad.Logical.lift
-
-
diff --git a/proofs/proofview.mli b/proofs/proofview.mli
index b1447e8ba..8e47878fa 100644
--- a/proofs/proofview.mli
+++ b/proofs/proofview.mli
@@ -411,12 +411,23 @@ module Refine : sig
   val new_evar : handle -> Environ.env -> Constr.types -> handle * Constr.t
   (** Create a new hole that will be added to the goals to solve. *)
 
+  val fresh_constructor_instance :
+    handle -> Environ.env -> Names.constructor -> handle * Constr.pconstructor
+  (** Creates a constructor with fresh universe variables. *)
+
+  val with_type : handle -> Environ.env -> Term.constr -> Term.types -> handle*Term.constr
+  (** [with_type h env c t] coerces refinable term [c] to type [t]. *)
+
   val refine : (handle -> handle * Constr.t) -> unit tactic
   (** Given a term with holes that have been generated through {!new_evar}, this
       function fills the current hole with the given constr and creates goals
       for all the holes in their generation order. Exceptions raised by the
       function are caught. *)
 
+  val refine_casted : (handle -> handle * Constr.t) -> unit tactic
+  (** Like {!refine} except the refined term is coerced to has, as its
+      type, the conclusion of the current goal. *)
+
 end
 
 (* The [NonLogical] module allows to execute side effects in tactics