Moving Refine to its proper module.

1 files changed, 2 insertions, 115 deletions

diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index f42a60d9db..20be02e76d 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