Removing the last use of tclSENSITIVE in favour of tclNEWGOALS.

Most of the code from Goal.Refine and related was moved to the one
file that was using it, wiz. tactics.ml. Some additional care should
be taken to clean up even more the remaining code.

5 files changed, 39 insertions, 131 deletions

diff --git a/proofs/goal.ml b/proofs/goal.ml
index dea704a68..b0fccc42f 100644
--- a/proofs/goal.ml
+++ b/proofs/goal.ml
@@ -125,9 +125,6 @@ let partition_unifiable sigma l =
 (*** Goal tactics ***)
 
 
-(* Goal tactics are [subgoal sensitive]-s *)
-type subgoals = { subgoals: goal list }
-
 (* type of the base elements of the goal API.*)
 (* it has an extra evar_info with respect to what would be expected,
    it is supposed to be the evar_info of the goal in the evar_map.
@@ -153,96 +150,6 @@ let bind e f = (); fun env rdefs goal info ->
   let r = f a in
   r env rdefs goal info
 
-(* Type of constr with holes used by refine. *)
-(* The list of evars doesn't necessarily contain all the evars in the constr,
-    only those the constr has introduced. *)
-(* The variables in [myevars] are supposed to be stored
-   in decreasing order. Breaking this invariant might cause
-   many things to go wrong. *)
-type refinable = {
-  me: constr;
-  my_evars: Evd.evar list
-}
-
-module Refinable = struct
-
-  let make t = (); fun env rdefs gl info ->
-    let r = ref [] in
-    let me = t r in
-    let me = me env rdefs gl info in
-    { me = me; my_evars = !r }
-
-  (* [with_type c typ] constrains term [c] to have type [typ].  *)
-  let with_type t typ = (); fun env rdefs _ _ ->
-    (* spiwack: this function assumes that no evars can be created during
-        this sort of coercion.
-        If it is not the case it could produce bugs. We would need to add a handle
-        and add the new evars to it. *)
-    let my_type = Retyping.get_type_of env !rdefs t in
-    let j = Environ.make_judge t my_type in
-    let (new_defs,j') =
-      Coercion.inh_conv_coerce_to true (Loc.ghost) env !rdefs j typ
-    in
-    rdefs := new_defs;
-    j'.Environ.uj_val
-
-  (* a pessimistic (i.e : there won't be many positive answers) filter
-     over evar_maps, acting only on undefined evars *)
-  let evar_map_filter_undefined f evm =
-    let fold ev evi accu = if f ev evi then ev :: accu else accu in
-    (** We rely on the LTR order of fold here... *)
-    Evar.Map.fold fold (Evd.undefined_map evm) []
-
-  (* Union, sorted in decreasing order, of two lists of evars in decreasing order. *)
-  let rec fusion l1 l2 = match l1 , l2 with
-    | [] , _ -> l2
-    | _ , [] -> l1
-    | a::l1 , b::_ when a > b -> a::(fusion l1 l2)
-    | a::l1 , b::l2 when Evar.equal a b -> a::(fusion l1 l2)
-    | _ , b::l2 -> b::(fusion l1 l2)
-
-  let update_handle handle init_defs post_defs =
-    (* [delta_list] holds the evars that have been introduced by this
-       refinement (but not immediatly solved) *)
-    let filter ev _ = not (Evd.mem init_defs ev) in
-    (* spiwack: this is the hackish part, don't know how to do any better though. *)
-    let delta_list = evar_map_filter_undefined filter post_defs in
-    (* The variables in [myevars] are supposed to be stored
-       in decreasing order. Breaking this invariant might cause
-       many things to go wrong. *)
-    handle := fusion delta_list !handle
-
-  let constr_of_open_constr handle check_type (evars, c) = (); fun env rdefs gl info ->
-    let () = update_handle handle !rdefs evars in
-    rdefs := Evd.fold (fun ev evi evd -> if not (Evd.mem !rdefs ev) then Evd.add evd ev evi else evd) evars !rdefs;
-    if check_type then with_type c (Evd.evar_concl (content !rdefs gl)) env rdefs gl info
-    else c
-
-end
-
-(* [refine t] takes a refinable term and use it as a partial proof for current
-    goal. *)
-let refine step = (); fun env rdefs gl info ->
-  (* subgoals to return *)
-  (* The evars in [my_evars] are stored in reverse order.
-     It is expectingly better however to display the goal
-     in increasing order. *)
-  rdefs := Evarconv.consider_remaining_unif_problems env !rdefs ;
-  let subgoals = List.map (descendent gl) (List.rev step.my_evars) in
-  (* creates the new [evar_map] by defining the evar of the current goal
-     as being [refine_step]. *)
-  let new_defs = Evd.define gl.content (step.me) !rdefs in
-  rdefs := new_defs;
-  (* Filtering the [subgoals] for uninstanciated (=unsolved) goals. *)
-  let subgoals =
-    Option.List.flatten (List.map (advance !rdefs) subgoals)
-  in
-  { subgoals = subgoals }
-
-let refine_open_constr c =
-  let pf h = Refinable.constr_of_open_constr h true c in
-  bind (Refinable.make pf) refine
-
 let enter f = (); fun env rdefs gl info ->
   let sigma = !rdefs in
   f env sigma (Evd.evar_concl info) gl
diff --git a/proofs/goal.mli b/proofs/goal.mli
index 4b85ec20b..4d4d0c2eb 100644
--- a/proofs/goal.mli
+++ b/proofs/goal.mli
@@ -120,9 +120,6 @@ end
 
 (*** Goal tactics. DEPRECATED. ***)
 
-(* Goal tactics are [subgoal sensitive]-s *)
-type subgoals = private { subgoals: goal list }
-
 (* Goal sensitive values *)
 type +'a sensitive
 
@@ -131,8 +128,6 @@ val eval :
   'a sensitive -> Environ.env -> Evd.evar_map -> goal ->
     'a * Evd.evar_map
 
-val refine_open_constr : Evd.open_constr -> subgoals sensitive
-
 (* [enter] combines [env], [defs], [hyps] and [concl] in a single
    primitive. *)
 val enter : (Environ.env -> Evd.evar_map -> Term.constr -> goal -> 'a) -> 'a sensitive
diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index e63db14ab..931d4a2b3 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -545,33 +545,6 @@ let tclNEWGOALS gls =
   { step with comb = step.comb @ gls }
   end
 
-(* No backtracking can happen here, hence, as opposed to the dispatch tacticals,
-    everything is done in one step. *)
-let sensitive_on_proofview s env step =
-  let wrap g ((defs, partial_list) as partial_res) = 
-    match Goal.advance defs g with
-    | None -> partial_res
-    | Some g ->
-      let { Goal.subgoals = sg } , d' = Goal.eval s env defs g in
-      (d', sg::partial_list)
-  in
-  let ( new_defs , combed_subgoals ) = 
-    List.fold_right wrap step.comb (step.solution,[])
-  in
-  { solution = new_defs; comb = List.flatten combed_subgoals; }
-
-let tclSENSITIVE s =
-  (* spiwack: convenience notations, waiting for ocaml 3.12 *)
-  let (>>=) = Proof.bind in
-  Proof.current >>= fun env ->
-  Proof.get >>= fun step ->
-  try
-    let next = sensitive_on_proofview s env step in
-    Proof.set next
-  with e when catchable_exception e ->
-    let e = Errors.push e in
-    tclZERO e
-
 let tclPROGRESS t =
   (* spiwack: convenience notations, waiting for ocaml 3.12 *)
   let (>>=) = Proof.bind in
diff --git a/proofs/proofview.mli b/proofs/proofview.mli
index cdc2db796..a1213cde2 100644
--- a/proofs/proofview.mli
+++ b/proofs/proofview.mli
@@ -235,10 +235,6 @@ val tclEXTEND : unit tactic list -> unit tactic -> unit tactic list -> unit tact
    backtracking in another. *)
 val tclINDEPENDENT : unit tactic -> unit tactic
 
-(* [tclSENSITIVE] views goal-type tactics as a special kind of tactics.*)
-val tclSENSITIVE : Goal.subgoals Goal.sensitive -> unit tactic 
-
-
 (* [tclPROGRESS t] behaves has [t] as long as [t] progresses. *)
 val tclPROGRESS : 'a tactic -> 'a tactic
 
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index f14810482..d06d78165 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -4203,6 +4203,38 @@ module Simple = struct
 
 end
 
+
+(* [with_type c typ] constrains term [c] to have type [typ].  *)
+let with_type t typ env sigma =
+  (* spiwack: this function assumes that no evars can be created during
+      this sort of coercion.
+      If it is not the case it could produce bugs. We would need to add a handle
+      and add the new evars to it. *)
+  let my_type = Retyping.get_type_of env sigma t in
+  let j = Environ.make_judge t my_type in
+  let (sigma, j') =
+    Coercion.inh_conv_coerce_to true (Loc.ghost) env sigma j typ
+  in
+  (sigma, j'.Environ.uj_val)
+
+let update_handle handle init_defs post_defs =
+  let filter ev _ = not (Evd.mem init_defs ev) in
+  let fold ev evi accu = if filter ev evi then Evar.Set.add ev accu else accu in
+  Evd.fold_undefined fold post_defs handle
+
+let constr_of_open_constr handle (evars, c) env sigma concl =
+  let () = handle := update_handle !handle sigma evars in
+  let fold ev evi evd = if not (Evd.mem sigma ev) then Evd.add evd ev evi else evd in
+  let sigma = Evd.fold fold evars sigma in
+  with_type c concl env sigma
+
+let refine_open_constr c env sigma concl =
+  let handle = ref Evar.Set.empty in
+  let sigma, pf = constr_of_open_constr handle c env sigma concl in
+  let sigma = Evarconv.consider_remaining_unif_problems env sigma in
+  let subgoals = List.map Goal.build (Evar.Set.elements !handle) in
+  (subgoals, pf, sigma)
+
 (** Tacticals defined directly in term of Proofview *)
 module New = struct
   open Proofview.Notations
@@ -4214,8 +4246,13 @@ module New = struct
 
   let refine c =
     Proofview.Goal.nf_enter begin fun gl ->
-    let pf = Goal.refine_open_constr c in
-    Proofview.tclSENSITIVE pf <*>
+    let env = Proofview.Goal.env gl in
+    let sigma = Proofview.Goal.sigma gl in
+    let concl = Proofview.Goal.concl gl in
+    let (gls, pf, sigma) = refine_open_constr c env sigma concl in
+    Proofview.V82.tclEVARS sigma <*>
+    Proofview.Refine.refine ~unsafe:true (fun h -> (h, pf)) <*>
+    Proofview.tclNEWGOALS gls <*>
       Proofview.V82.tactic (reduce
          (Lazy {rBeta=true;rIota=true;rZeta=false;rDelta=false;rConst=[]})
          {onhyps=None; concl_occs=AllOccurrences }