Moving Refine to its proper module.

14 files changed, 209 insertions, 186 deletions

diff --git a/dev/printers.mllib b/dev/printers.mllib
index 7710033db..c46f6b72a 100644
--- a/dev/printers.mllib
+++ b/dev/printers.mllib
@@ -184,6 +184,7 @@ Proof_errors
 Logic_monad
 Proofview_monad
 Proofview
+Refine
 Proof
 Proof_global
 Pfedit
diff --git a/printing/printer.ml b/printing/printer.ml
index b89005887..2e67fa5ff 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -50,7 +50,7 @@ let pr_lconstr_core goal_concl_style env sigma t =
 
 let pr_lconstr_env env = pr_lconstr_core false env
 let pr_constr_env env = pr_constr_core false env
-let _ = Hook.set Proofview.Refine.pr_constr pr_constr_env
+let _ = Hook.set Refine.pr_constr pr_constr_env
 
 let pr_lconstr_goal_style_env env = pr_lconstr_core true env
 let pr_constr_goal_style_env env = pr_constr_core true env
diff --git a/proofs/proof.ml b/proofs/proof.ml
index b604fde4e..86af420dc 100644
--- a/proofs/proof.ml
+++ b/proofs/proof.ml
@@ -334,22 +334,24 @@ let compact p =
 (*** Tactics ***)
 
 let run_tactic env tac pr =
+  let open Proofview.Notations in
   let sp = pr.proofview in
-  let (_,tacticced_proofview,(status,to_shelve,give_up),info_trace) =
-    Proofview.apply env tac sp
+  let undef sigma l = List.filter (fun g -> Evd.is_undefined sigma g) l in
+  let tac =
+    tac >>= fun () ->
+    Proofview.tclEVARMAP >>= fun sigma ->
+    (* Already solved goals are not to be counted as shelved. Nor are
+      they to be marked as unresolvable. *)
+    let retrieved = undef sigma (List.rev (Evd.future_goals sigma)) in
+    let sigma = List.fold_left Proofview.Unsafe.mark_as_goal sigma retrieved in
+    Proofview.Unsafe.tclEVARS sigma >>= fun () ->
+    Proofview.tclUNIT retrieved
   in
-  let sigma = Proofview.return tacticced_proofview in
-  (* Already solved goals are not to be counted as shelved. Nor are
-     they to be marked as unresolvable. *)
-  let undef l = List.filter (fun g -> Evd.is_undefined sigma g) l in
-  let retrieved = undef (List.rev (Evd.future_goals sigma)) in
-  let shelf = (undef pr.shelf)@retrieved@(undef to_shelve) in
-  let proofview =
-    List.fold_left
-      Proofview.Unsafe.mark_as_goal
-      tacticced_proofview
-      retrieved
+  let (retrieved,proofview,(status,to_shelve,give_up),info_trace) =
+    Proofview.apply env tac sp
   in
+  let sigma = Proofview.return proofview in
+  let shelf = (undef sigma pr.shelf)@retrieved@(undef sigma to_shelve) in
   let given_up = pr.given_up@give_up in
   let proofview = Proofview.Unsafe.reset_future_goals proofview in
   { pr with proofview ; shelf ; given_up },(status,info_trace)
diff --git a/proofs/proofs.mllib b/proofs/proofs.mllib
index 08556d62e..236d47932 100644
--- a/proofs/proofs.mllib
+++ b/proofs/proofs.mllib
@@ -5,6 +5,7 @@ Proof_using
 Proof_errors
 Logic
 Proofview
+Refine
 Proof
 Proof_global
 Redexpr
diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index f42a60d9d..20be02e76 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -901,7 +901,7 @@ module Unsafe = struct
   let reset_future_goals p =
     { p with solution = Evd.reset_future_goals p.solution }
 
-  let mark_as_goal_evm evd content =
+  let mark_as_goal evd content =
     let info = Evd.find evd content in
     let info =
       { info with Evd.evar_source = match info.Evd.evar_source with
@@ -911,8 +911,7 @@ module Unsafe = struct
     let info = Typeclasses.mark_unresolvable info in
     Evd.add evd content info
 
-  let mark_as_goal p gl =
-    { p with solution = mark_as_goal_evm p.solution gl }
+  let advance = advance
 
 end
 
@@ -1075,118 +1074,6 @@ end
 
 
 
-(** {6 The refine tactic} *)
-
-module Refine =
-struct
-
-  let extract_prefix env info =
-    let ctx1 = List.rev (Environ.named_context env) in
-    let ctx2 = List.rev (Evd.evar_context info) in
-    let rec share l1 l2 accu = match l1, l2 with
-    | d1 :: l1, d2 :: l2 ->
-      if d1 == d2 then share l1 l2 (d1 :: accu)
-      else (accu, d2 :: l2)
-    | _ -> (accu, l2)
-    in
-    share ctx1 ctx2 []
-
-  let typecheck_evar ev env sigma =
-    let info = Evd.find sigma ev in
-    (** Typecheck the hypotheses. *)
-    let type_hyp (sigma, env) decl =
-      let t = get_type decl in
-      let evdref = ref sigma in
-      let _ = Typing.e_sort_of env evdref t in
-      let () = match decl with
-      | LocalAssum _ -> ()
-      | LocalDef (_,body,_) -> Typing.e_check env evdref body t
-      in
-      (!evdref, Environ.push_named decl env)
-    in
-    let (common, changed) = extract_prefix env info in
-    let env = Environ.reset_with_named_context (Environ.val_of_named_context common) env in
-    let (sigma, env) = List.fold_left type_hyp (sigma, env) changed in
-    (** Typecheck the conclusion *)
-    let evdref = ref sigma in
-    let _ = Typing.e_sort_of env evdref (Evd.evar_concl info) in
-    !evdref
-
-  let typecheck_proof c concl env sigma =
-    let evdref = ref sigma in
-    let () = Typing.e_check env evdref c concl in
-    !evdref
-
-  let (pr_constrv,pr_constr) =
-    Hook.make ~default:(fun _env _sigma _c -> Pp.str"<constr>") ()
-
-  let refine ?(unsafe = true) f = Goal.enter { Goal.enter = begin fun gl ->
-    let sigma = Goal.sigma gl in
-    let sigma = Sigma.to_evar_map sigma in
-    let env = Goal.env gl in
-    let concl = Goal.concl gl in
-    (** Save the [future_goals] state to restore them after the
-        refinement. *)
-    let prev_future_goals = Evd.future_goals sigma in
-    let prev_principal_goal = Evd.principal_future_goal sigma in
-    (** Create the refinement term *)
-    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 *)
-    let fold accu ev = typecheck_evar ev env accu in
-    let sigma = if unsafe then sigma else CList.fold_left fold sigma evs in
-    (** Check that the refined term is typesafe *)
-    let sigma = if unsafe then sigma else typecheck_proof c concl env sigma in
-    (** Check that the goal itself does not appear in the refined term *)
-    let _ =
-      if not (Evarutil.occur_evar_upto sigma gl.Goal.self c) then ()
-      else Pretype_errors.error_occur_check env sigma gl.Goal.self c
-    in
-    (** Proceed to the refinement *)
-    let sigma = match evkmain with
-      | None -> Evd.define gl.Goal.self c sigma
-      | Some evk ->
-          let id = Evd.evar_ident gl.Goal.self sigma in
-          let sigma = Evd.define gl.Goal.self c sigma in
-          match id with
-          | None -> sigma
-          | Some id -> Evd.rename evk id sigma
-    in
-    (** Restore the [future goals] state. *)
-    let sigma = Evd.restore_future_goals sigma prev_future_goals prev_principal_goal in
-    (** Select the goals *)
-    let comb = undefined sigma (CList.rev evs) in
-    let sigma = CList.fold_left Unsafe.mark_as_goal_evm sigma comb in
-    let open Proof in
-    InfoL.leaf (Info.Tactic (fun () -> Pp.(hov 2 (str"refine"++spc()++ Hook.get pr_constrv env sigma c)))) >>
-    Pv.modify (fun ps -> { ps with solution = sigma; comb; })
-  end }
-
-  (** Useful definitions *)
-
-  let with_type env evd 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 , j'.Environ.uj_val
-
-  let refine_casted ?unsafe f = Goal.enter { Goal.enter = begin fun gl ->
-    let concl = Goal.concl gl in
-    let env = 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
-      Sigma (c, Sigma.Unsafe.of_evar_map sigma, p)
-    } in
-    refine ?unsafe f
-  end }
-end
-
-
-
 (** {6 Trace} *)
 
 module Trace = struct
diff --git a/proofs/proofview.mli b/proofs/proofview.mli
index 20f67f258..6bc2e9a0e 100644
--- a/proofs/proofview.mli
+++ b/proofs/proofview.mli
@@ -406,7 +406,13 @@ module Unsafe : sig
 
   (** Give an evar the status of a goal (changes its source location
       and makes it unresolvable for type classes. *)
-  val mark_as_goal : proofview -> Evar.t -> proofview
+  val mark_as_goal : Evd.evar_map -> Evar.t -> Evd.evar_map
+
+  (** [advance sigma g] returns [Some g'] if [g'] is undefined and is
+      the current avatar of [g] (for instance [g] was changed by [clear]
+      into [g']). It returns [None] if [g] has been (partially)
+      solved. *)
+  val advance : Evd.evar_map -> Evar.t -> Evar.t option
 end
 
 (** This module gives access to the innards of the monad. Its use is
@@ -491,39 +497,6 @@ module Goal : sig
 end
 
 
-(** {6 The refine tactic} *)
-
-module Refine : sig
-
-  (** Printer used to print the constr which refine refines. *)
-  val pr_constr :
-    (Environ.env -> Evd.evar_map -> Term.constr -> Pp.std_ppcmds) Hook.t
-
-  (** {7 Refinement primitives} *)
-
-  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
-      new holes created by [t] become the new subgoals. Exceptions
-      raised during the interpretation of [t] are caught and result in
-      tactic failures. If [unsafe] is [false] (default is [true]) [t] is
-      type-checked beforehand. *)
-
-  (** {7 Helper functions} *)
-
-  val with_type : Environ.env -> Evd.evar_map ->
-    Term.constr -> Term.types -> Evd.evar_map * Term.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
-  (** Like {!refine} except the refined term is coerced to the conclusion of the
-      current goal. *)
-
-end
-
-
 (** {6 Trace} *)
 
 module Trace : sig
diff --git a/proofs/refine.ml b/proofs/refine.ml
new file mode 100644
index 000000000..db0b26f7e
--- /dev/null
+++ b/proofs/refine.ml
@@ -0,0 +1,122 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+open Pp
+open Util
+open Proofview_monad
+open Sigma.Notations
+open Proofview.Notations
+open Context.Named.Declaration
+
+let extract_prefix env info =
+  let ctx1 = List.rev (Environ.named_context env) in
+  let ctx2 = List.rev (Evd.evar_context info) in
+  let rec share l1 l2 accu = match l1, l2 with
+  | d1 :: l1, d2 :: l2 ->
+    if d1 == d2 then share l1 l2 (d1 :: accu)
+    else (accu, d2 :: l2)
+  | _ -> (accu, l2)
+  in
+  share ctx1 ctx2 []
+
+let typecheck_evar ev env sigma =
+  let info = Evd.find sigma ev in
+  (** Typecheck the hypotheses. *)
+  let type_hyp (sigma, env) decl =
+    let t = get_type decl in
+    let evdref = ref sigma in
+    let _ = Typing.e_sort_of env evdref t in
+    let () = match decl with
+    | LocalAssum _ -> ()
+    | LocalDef (_,body,_) -> Typing.e_check env evdref body t
+    in
+    (!evdref, Environ.push_named decl env)
+  in
+  let (common, changed) = extract_prefix env info in
+  let env = Environ.reset_with_named_context (Environ.val_of_named_context common) env in
+  let (sigma, env) = List.fold_left type_hyp (sigma, env) changed in
+  (** Typecheck the conclusion *)
+  let evdref = ref sigma in
+  let _ = Typing.e_sort_of env evdref (Evd.evar_concl info) in
+  !evdref
+
+let typecheck_proof c concl env sigma =
+  let evdref = ref sigma in
+  let () = Typing.e_check env evdref c concl in
+  !evdref
+
+let (pr_constrv,pr_constr) =
+  Hook.make ~default:(fun _env _sigma _c -> Pp.str"<constr>") ()
+
+let refine ?(unsafe = true) f = Proofview.Goal.enter { enter = begin fun gl ->
+  let gl = Proofview.Goal.assume gl in
+  let sigma = Proofview.Goal.sigma gl in
+  let sigma = Sigma.to_evar_map sigma in
+  let env = Proofview.Goal.env gl in
+  let concl = Proofview.Goal.concl gl in
+  (** Save the [future_goals] state to restore them after the
+      refinement. *)
+  let prev_future_goals = Evd.future_goals sigma in
+  let prev_principal_goal = Evd.principal_future_goal sigma in
+  (** Create the refinement term *)
+  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 *)
+  let fold accu ev = typecheck_evar ev env accu in
+  let sigma = if unsafe then sigma else CList.fold_left fold sigma evs in
+  (** Check that the refined term is typesafe *)
+  let sigma = if unsafe then sigma else typecheck_proof c concl env sigma in
+  (** Check that the goal itself does not appear in the refined term *)
+  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 c
+  in
+  (** Proceed to the refinement *)
+  let sigma = match evkmain with
+    | None -> Evd.define self c sigma
+    | Some evk ->
+        let id = Evd.evar_ident self sigma in
+        let sigma = Evd.define self c sigma in
+        match id with
+        | None -> sigma
+        | Some id -> Evd.rename evk id sigma
+  in
+  (** Restore the [future goals] state. *)
+  let sigma = Evd.restore_future_goals sigma prev_future_goals prev_principal_goal in
+  (** Select the goals *)
+  let comb = CList.map_filter (Proofview.Unsafe.advance sigma) (CList.rev evs) in
+  let sigma = CList.fold_left Proofview.Unsafe.mark_as_goal sigma comb in
+  let trace () = Pp.(hov 2 (str"refine"++spc()++ Hook.get pr_constrv env sigma c)) in
+  Proofview.Trace.name_tactic trace (Proofview.tclUNIT ()) >>= fun () ->
+  Proofview.Unsafe.tclEVARS sigma >>= fun () ->
+  Proofview.Unsafe.tclSETGOALS comb
+end }
+
+(** Useful definitions *)
+
+let with_type env evd 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 , 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 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
+    Sigma (c, Sigma.Unsafe.of_evar_map sigma, p)
+  } in
+  refine ?unsafe f
+end }
diff --git a/proofs/refine.mli b/proofs/refine.mli
new file mode 100644
index 000000000..17c7e28ca
--- /dev/null
+++ b/proofs/refine.mli
@@ -0,0 +1,37 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+open Proofview
+
+(** {6 The refine tactic} *)
+
+(** Printer used to print the constr which refine refines. *)
+val pr_constr :
+  (Environ.env -> Evd.evar_map -> Term.constr -> Pp.std_ppcmds) Hook.t
+
+(** {7 Refinement primitives} *)
+
+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
+    new holes created by [t] become the new subgoals. Exceptions
+    raised during the interpretation of [t] are caught and result in
+    tactic failures. If [unsafe] is [false] (default is [true]) [t] is
+    type-checked beforehand. *)
+
+(** {7 Helper functions} *)
+
+val with_type : Environ.env -> Evd.evar_map ->
+  Term.constr -> Term.types -> Evd.evar_map * Term.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
+(** Like {!refine} except the refined term is coerced to the conclusion of the
+    current goal. *)
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index 0cc796886..23aa8dcb4 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -370,7 +370,7 @@ let refine_tac ist simple c =
     let expected_type = Pretyping.OfType concl in
     let c = Tacinterp.type_uconstr ~flags ~expected_type ist c in
     let update = { run = fun sigma -> c.delayed env sigma } in
-    let refine = Proofview.Refine.refine ~unsafe:false update in
+    let refine = Refine.refine ~unsafe:false update in
     if simple then refine
     else refine <*>
            Tactics.New.reduce_after_refine <*>
diff --git a/tactics/inv.ml b/tactics/inv.ml
index 6841ab0ec..89c6beb32 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -459,7 +459,7 @@ let raw_inversion inv_kind id status names =
     in
     let refined id =
       let prf = mkApp (mkVar id, args) in
-      Proofview.Refine.refine { run = fun h -> Sigma (prf, h, Sigma.refl) }
+      Refine.refine { run = fun h -> Sigma (prf, h, Sigma.refl) }
     in
     let neqns = List.length realargs in
     let as_mode = names != None in
diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml
index 67d21886b..4c06550d4 100644
--- a/tactics/rewrite.ml
+++ b/tactics/rewrite.ml
@@ -1539,7 +1539,7 @@ let assert_replacing id newt tac =
     | d :: rem -> insert_dependent env (LocalAssum (get_id d, newt)) [] after @ rem
     in
     let env' = Environ.reset_with_named_context (val_of_named_context nc) env in
-    Proofview.Refine.refine ~unsafe:false { run = begin fun sigma ->
+    Refine.refine ~unsafe:false { run = begin fun sigma ->
       let Sigma (ev, sigma, p) = Evarutil.new_evar env' sigma concl in
       let Sigma (ev', sigma, q) = Evarutil.new_evar env sigma newt in
       let map d =
@@ -1568,7 +1568,7 @@ let cl_rewrite_clause_newtac ?abs ?origsigma ~progress strat clause =
         let gls = List.rev (Evd.fold_undefined fold undef []) in
 	match clause, prf with
 	| Some id, Some p ->
-            let tac = Proofview.Refine.refine ~unsafe:false { run = fun h -> Sigma (p, h, Sigma.refl) } <*> Proofview.Unsafe.tclNEWGOALS gls in
+            let tac = Refine.refine ~unsafe:false { run = fun h -> Sigma (p, h, Sigma.refl) } <*> Proofview.Unsafe.tclNEWGOALS gls in
             Proofview.Unsafe.tclEVARS undef <*>
 	    assert_replacing id newt tac
 	| Some id, None ->
@@ -1582,7 +1582,7 @@ let cl_rewrite_clause_newtac ?abs ?origsigma ~progress strat clause =
               let Sigma (ev, sigma, q) = Evarutil.new_evar env sigma newt in
               Sigma (mkApp (p, [| ev |]), sigma, q)
             end } in
-            Proofview.Refine.refine ~unsafe:false make <*> Proofview.Unsafe.tclNEWGOALS gls
+            Refine.refine ~unsafe:false make <*> Proofview.Unsafe.tclNEWGOALS gls
             end }
 	| None, None ->
             Proofview.Unsafe.tclEVARS undef <*>
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index ffe10d81c..7ae178af5 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -163,7 +163,7 @@ let _ =
     does not check anything. *)
 let unsafe_intro env store decl b =
   let open Context.Named.Declaration in
-  Proofview.Refine.refine ~unsafe:true { run = begin fun sigma ->
+  Refine.refine ~unsafe:true { run = begin fun sigma ->
     let ctx = named_context_val env in
     let nctx = push_named_context_val decl ctx in
     let inst = List.map (mkVar % get_id) (named_context env) in
@@ -199,7 +199,7 @@ let convert_concl ?(check=true) ty k =
     let env = Proofview.Goal.env gl in
     let store = Proofview.Goal.extra gl in
     let conclty = Proofview.Goal.raw_concl gl in
-    Proofview.Refine.refine ~unsafe:true { run = begin fun sigma ->
+    Refine.refine ~unsafe:true { run = begin fun sigma ->
       let Sigma ((), sigma, p) =
         if check then begin
           let sigma = Sigma.to_evar_map sigma in
@@ -222,7 +222,7 @@ let convert_hyp ?(check=true) d =
     let store = Proofview.Goal.extra gl in
     let sign = convert_hyp check (named_context_val env) sigma d in
     let env = reset_with_named_context sign env in
-    Proofview.Refine.refine ~unsafe:true { run = begin fun sigma ->
+    Refine.refine ~unsafe:true { run = begin fun sigma ->
       Evarutil.new_evar env sigma ~principal:true ~store ty
     end }
   end }
@@ -345,7 +345,7 @@ let rename_hyp repl =
       let nconcl = subst concl in
       let nctx = Environ.val_of_named_context nhyps in
       let instance = List.map (mkVar % get_id) hyps in
-      Proofview.Refine.refine ~unsafe:true { run = begin fun sigma ->
+      Refine.refine ~unsafe:true { run = begin fun sigma ->
         Evarutil.new_evar_instance nctx sigma nconcl ~store instance
       end }
     end }
@@ -1070,7 +1070,7 @@ let cut c =
       let id = next_name_away_with_default "H" Anonymous (Tacmach.New.pf_ids_of_hyps gl) in
       (** Backward compat: normalize [c]. *)
       let c = if normalize_cut then local_strong whd_betaiota sigma c else c in
-      Proofview.Refine.refine ~unsafe:true { run = begin fun h ->
+      Refine.refine ~unsafe:true { run = begin fun h ->
         let Sigma (f, h, p) = Evarutil.new_evar ~principal:true env h (mkArrow c (Vars.lift 1 concl)) in
         let Sigma (x, h, q) = Evarutil.new_evar env h c in
         let f = mkLetIn (Name id, x, c, mkApp (Vars.lift 1 f, [|mkRel 1|])) in
@@ -1736,7 +1736,7 @@ let cut_and_apply c =
       | Prod (_,c1,c2) when not (dependent (mkRel 1) c2) ->
         let concl = Proofview.Goal.concl gl in
         let env = Tacmach.New.pf_env gl in
-        Proofview.Refine.refine { run = begin fun sigma ->
+        Refine.refine { run = begin fun sigma ->
           let typ = mkProd (Anonymous, c2, concl) in
           let Sigma (f, sigma, p) = Evarutil.new_evar env sigma typ in
           let Sigma (x, sigma, q) = Evarutil.new_evar env sigma c1 in
@@ -1757,7 +1757,7 @@ let cut_and_apply c =
 (* let refine_no_check = Profile.profile2 refine_no_checkkey refine_no_check *)
 
 let new_exact_no_check c =
-  Proofview.Refine.refine ~unsafe:true { run = fun h -> Sigma.here c h }
+  Refine.refine ~unsafe:true { run = fun h -> Sigma.here c h }
 
 let exact_check c =
   Proofview.Goal.s_enter { s_enter = begin fun gl ->
@@ -1808,7 +1808,7 @@ let assumption =
     in
     if is_same_type then
       (Proofview.Unsafe.tclEVARS sigma) <*>
-	Proofview.Refine.refine ~unsafe:true { run = fun h -> Sigma.here (mkVar (get_id decl)) h }
+	Refine.refine ~unsafe:true { run = fun h -> Sigma.here (mkVar (get_id decl)) h }
     else arec gl only_eq rest
   in
   let assumption_tac = { enter = begin fun gl ->
@@ -1893,7 +1893,7 @@ let clear_body ids =
       check_is_type env concl msg
     in
     check_hyps <*> check_concl <*>
-    Proofview.Refine.refine ~unsafe:true { run = begin fun sigma ->
+    Refine.refine ~unsafe:true { run = begin fun sigma ->
       Evarutil.new_evar env sigma ~principal:true concl
     end }
   end }
@@ -1950,7 +1950,7 @@ let apply_type newcl args =
   Proofview.Goal.enter { enter = begin fun gl ->
     let env = Proofview.Goal.env gl in
     let store = Proofview.Goal.extra gl in
-    Proofview.Refine.refine { run = begin fun sigma ->
+    Refine.refine { run = begin fun sigma ->
       let newcl = nf_betaiota (Sigma.to_evar_map sigma) newcl (* As in former Logic.refine *) in
       let Sigma (ev, sigma, p) =
         Evarutil.new_evar env sigma ~principal:true ~store newcl in
@@ -1971,7 +1971,7 @@ let bring_hyps hyps =
       let concl = Tacmach.New.pf_nf_concl gl in
       let newcl = List.fold_right mkNamedProd_or_LetIn hyps concl in
       let args = Array.of_list (Context.Named.to_instance hyps) in
-      Proofview.Refine.refine { run = begin fun sigma ->
+      Refine.refine { run = begin fun sigma ->
         let Sigma (ev, sigma, p) =
           Evarutil.new_evar env sigma ~principal:true ~store newcl in
         Sigma (mkApp (ev, args), sigma, p)
@@ -2671,7 +2671,7 @@ let new_generalize_gen_let lconstr =
 	0 lconstr (concl, sigma, [])
     in
     let tac =
-	Proofview.Refine.refine { run = begin fun sigma ->
+	Refine.refine { run = begin fun sigma ->
           let Sigma (ev, sigma, p) = Evarutil.new_evar env sigma ~principal:true newcl in
           Sigma ((applist (ev, args)), sigma, p)
 	end }
@@ -3325,7 +3325,7 @@ let mk_term_eq env sigma ty t ty' t' =
 
 let make_abstract_generalize env id typ concl dep ctx body c eqs args refls =
   let open Context.Rel.Declaration in
-  Proofview.Refine.refine { run = begin fun sigma ->
+  Refine.refine { run = begin fun sigma ->
   let eqslen = List.length eqs in
     (* Abstract by the "generalized" hypothesis equality proof if necessary. *)
   let abshypeq, abshypt =
@@ -4126,7 +4126,7 @@ let pose_induction_arg_then isrec with_evars (is_arg_pure_hyp,from_prefix) elim
           (* and destruct has side conditions first *)
           Tacticals.New.tclTHENLAST)
       (Tacticals.New.tclTHENLIST [
-        Proofview.Refine.refine ~unsafe:true { run = begin fun sigma ->
+        Refine.refine ~unsafe:true { run = begin fun sigma ->
           let b = not with_evars && with_eq != None in
           let Sigma (c, sigma, p) = use_bindings env sigma elim b (c0,lbind) t0 in
           let t = Retyping.get_type_of env (Sigma.to_evar_map sigma) c in
@@ -4150,7 +4150,7 @@ let pose_induction_arg_then isrec with_evars (is_arg_pure_hyp,from_prefix) elim
       let env = reset_with_named_context sign env in
       let tac =
       Tacticals.New.tclTHENLIST [
-        Proofview.Refine.refine ~unsafe:true { run = begin fun sigma ->
+        Refine.refine ~unsafe:true { run = begin fun sigma ->
           mkletin_goal env sigma store with_eq true (id,lastlhyp,ccl,c) None
         end };
         tac
@@ -4795,6 +4795,6 @@ module New = struct
       {onhyps=None; concl_occs=AllOccurrences }
 
   let refine ?unsafe c =
-    Proofview.Refine.refine ?unsafe c <*>
+    Refine.refine ?unsafe c <*>
     reduce_after_refine
 end
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index 26ea01769..4c4a96ec0 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -431,7 +431,7 @@ end
 module New : sig
 
   val refine : ?unsafe:bool -> constr Sigma.run -> unit Proofview.tactic
-  (** [refine ?unsafe c] is [Proofview.Refine.refine ?unsafe c]
+  (** [refine ?unsafe c] is [Refine.refine ?unsafe c]
       followed by beta-iota-reduction of the conclusion. *)
 
   val reduce_after_refine : unit Proofview.tactic
diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index 0a83c49c8..4bf0450d2 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -330,7 +330,7 @@ let new_instance ?(abstract=false) ?(global=false) poly ctx (instid, bk, cl) pro
 		if not (Option.is_empty term) then
                   let init_refine =
                     Tacticals.New.tclTHENLIST [
-                      Proofview.Refine.refine { run = fun evm -> Sigma (Option.get term, evm, Sigma.refl) };
+                      Refine.refine { run = fun evm -> Sigma (Option.get term, evm, Sigma.refl) };
                       Proofview.Unsafe.tclNEWGOALS gls;
                       Tactics.New.reduce_after_refine;
                     ]