[proof] Merge `Pfedit` into proofs.

If we remove all the legacy proof engine stuff, that would remove the
need for the view on proof almost entirely.

15 files changed, 144 insertions, 171 deletions

diff --git a/plugins/ltac/extratactics.mlg b/plugins/ltac/extratactics.mlg
index c2023289a4..7ed733cf57 100644
--- a/plugins/ltac/extratactics.mlg
+++ b/plugins/ltac/extratactics.mlg
@@ -346,7 +346,7 @@ open Vars
 
 let constr_flags () = {
   Pretyping.use_typeclasses = Pretyping.UseTC;
-  Pretyping.solve_unification_constraints = Pfedit.use_unification_heuristics ();
+  Pretyping.solve_unification_constraints = Proof.use_unification_heuristics ();
   Pretyping.fail_evar = false;
   Pretyping.expand_evars = true;
   Pretyping.program_mode = false;
diff --git a/plugins/ltac/g_ltac.mlg b/plugins/ltac/g_ltac.mlg
index 0a46522543..3cc8c4934a 100644
--- a/plugins/ltac/g_ltac.mlg
+++ b/plugins/ltac/g_ltac.mlg
@@ -369,7 +369,7 @@ let vernac_solve ~pstate n info tcom b =
       let global = match n with SelectAll | SelectList _ -> true | _ -> false in
       let info = Option.append info (print_info_trace ()) in
       let (p,status) =
-        Pfedit.solve n info (Tacinterp.hide_interp global tcom None) ?with_end_tac p
+        Proof.solve n info (Tacinterp.hide_interp global tcom None) ?with_end_tac p
       in
       (* in case a strict subtree was completed,
          go back to the top of the prooftree *)
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index 321b05b97c..820063c25c 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -639,7 +639,7 @@ let solve_remaining_by env sigma holes by =
         let env = Environ.reset_with_named_context evi.evar_hyps env in
         let ty = evi.evar_concl in
         let name, poly = Id.of_string "rewrite", false in
-        let c, sigma = Pfedit.refine_by_tactic ~name ~poly env sigma ty solve_tac in
+        let c, sigma = Proof.refine_by_tactic ~name ~poly env sigma ty solve_tac in
         Evd.define evk (EConstr.of_constr c) sigma
     in
     List.fold_left solve sigma indep
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index b0e26e1def..dda7f0742c 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -2070,7 +2070,7 @@ let _ =
      *)
     let name, poly = Id.of_string "ltac_gen", poly in
     let name, poly = Id.of_string "ltac_gen", poly in
-    let (c, sigma) = Pfedit.refine_by_tactic ~name ~poly env sigma ty tac in
+    let (c, sigma) = Proof.refine_by_tactic ~name ~poly env sigma ty tac in
     (EConstr.of_constr c, sigma)
   in
   GlobEnv.register_constr_interp0 wit_tactic eval
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
deleted file mode 100644
index 20975cbc57..0000000000
--- a/proofs/pfedit.ml
+++ /dev/null
@@ -1,115 +0,0 @@
-(************************************************************************)
-(*         *   The Coq Proof Assistant / The Coq Development Team       *)
-(*  v      *         Copyright INRIA, CNRS and contributors             *)
-(* <O___,, * (see version control and CREDITS file for authors & dates) *)
-(*   \VV/  **************************************************************)
-(*    //   *    This file is distributed under the terms of the         *)
-(*         *     GNU Lesser General Public License Version 2.1          *)
-(*         *     (see LICENSE file for the text of the license)         *)
-(************************************************************************)
-
-open Pp
-open Util
-open Evd
-
-let use_unification_heuristics =
-  Goptions.declare_bool_option_and_ref
-    ~depr:false
-    ~key:["Solve";"Unification";"Constraints"]
-    ~value:true
-
-let solve ?with_end_tac gi info_lvl tac pr =
-    let tac = match with_end_tac with
-      | None -> tac
-      | Some etac -> Proofview.tclTHEN tac etac in
-    let tac = match info_lvl with
-      | None -> tac
-      | Some _ -> Proofview.Trace.record_info_trace tac
-    in
-    let nosuchgoal = Proofview.tclZERO (Proof_bullet.SuggestNoSuchGoals (1,pr)) in
-    let tac = let open Goal_select in match gi with
-      | SelectAlreadyFocused ->
-        let open Proofview.Notations in
-        Proofview.numgoals >>= fun n ->
-        if n == 1 then tac
-        else
-          let e = CErrors.UserError
-              (None,
-               Pp.(str "Expected a single focused goal but " ++
-                   int n ++ str " goals are focused."))
-          in
-          Proofview.tclZERO e
-
-      | SelectNth i -> Proofview.tclFOCUS ~nosuchgoal i i tac
-      | SelectList l -> Proofview.tclFOCUSLIST ~nosuchgoal l tac
-      | SelectId id -> Proofview.tclFOCUSID ~nosuchgoal id tac
-      | SelectAll -> tac
-    in
-    let tac =
-      if use_unification_heuristics () then
-        Proofview.tclTHEN tac Refine.solve_constraints
-      else tac
-    in
-    let env = Global.env () in
-    let (p,(status,info),()) = Proof.run_tactic env tac pr in
-    let env = Global.env () in
-    let sigma = Evd.from_env env in
-    let () =
-      match info_lvl with
-      | None -> ()
-      | Some i -> Feedback.msg_info (hov 0 (Proofview.Trace.pr_info env sigma ~lvl:i info))
-    in
-    (p,status)
-
-(**********************************************************************)
-(* Shortcut to build a term using tactics *)
-
-let refine_by_tactic ~name ~poly env sigma ty tac =
-  (* Save the initial side-effects to restore them afterwards. We set the
-     current set of side-effects to be empty so that we can retrieve the
-     ones created during the tactic invocation easily. *)
-  let eff = Evd.eval_side_effects sigma in
-  let sigma = Evd.drop_side_effects sigma in
-  (* Save the existing goals *)
-  let prev_future_goals = save_future_goals sigma in
-  (* Start a proof *)
-  let prf = Proof.start ~name ~poly sigma [env, ty] in
-  let (prf, _, ()) =
-    try Proof.run_tactic env tac prf
-    with Logic_monad.TacticFailure e as src ->
-      (* Catch the inner error of the monad tactic *)
-      let (_, info) = Exninfo.capture src in
-      Exninfo.iraise (e, info)
-  in
-  (* Plug back the retrieved sigma *)
-  let Proof.{ goals; stack; shelf; given_up; sigma; entry } = Proof.data prf in
-  assert (stack = []);
-  let ans = match Proofview.initial_goals entry with
-  | [c, _] -> c
-  | _ -> assert false
-  in
-  let ans = EConstr.to_constr ~abort_on_undefined_evars:false sigma ans in
-  (* [neff] contains the freshly generated side-effects *)
-  let neff = Evd.eval_side_effects sigma in
-  (* Reset the old side-effects *)
-  let sigma = Evd.drop_side_effects sigma in
-  let sigma = Evd.emit_side_effects eff sigma in
-  (* Restore former goals *)
-  let sigma = restore_future_goals sigma prev_future_goals in
-  (* Push remaining goals as future_goals which is the only way we
-     have to inform the caller that there are goals to collect while
-     not being encapsulated in the monad *)
-  (* Goals produced by tactic "shelve" *)
-  let sigma = List.fold_right (Evd.declare_future_goal ~tag:Evd.ToShelve) shelf sigma in
-  (* Goals produced by tactic "give_up" *)
-  let sigma = List.fold_right (Evd.declare_future_goal ~tag:Evd.ToGiveUp) given_up sigma in
-  (* Other goals *)
-  let sigma = List.fold_right Evd.declare_future_goal goals sigma in
-  (* Get rid of the fresh side-effects by internalizing them in the term
-     itself. Note that this is unsound, because the tactic may have solved
-     other goals that were already present during its invocation, so that
-     those goals rely on effects that are not present anymore. Hopefully,
-     this hack will work in most cases. *)
-  let neff = neff.Evd.seff_private in
-  let (ans, _) = Safe_typing.inline_private_constants env ((ans, Univ.ContextSet.empty), neff) in
-  ans, sigma
diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli
deleted file mode 100644
index 8d06a260da..0000000000
--- a/proofs/pfedit.mli
+++ /dev/null
@@ -1,41 +0,0 @@
-(************************************************************************)
-(*         *   The Coq Proof Assistant / The Coq Development Team       *)
-(*  v      *         Copyright INRIA, CNRS and contributors             *)
-(* <O___,, * (see version control and CREDITS file for authors & dates) *)
-(*   \VV/  **************************************************************)
-(*    //   *    This file is distributed under the terms of the         *)
-(*         *     GNU Lesser General Public License Version 2.1          *)
-(*         *     (see LICENSE file for the text of the license)         *)
-(************************************************************************)
-
-(** Global proof state. A quite redundant wrapper on {!Proof_global}. *)
-
-open Names
-open Constr
-open Environ
-
-(** {6 ... } *)
-
-(** [solve (SelectNth n) tac] applies tactic [tac] to the [n]th
-    subgoal of the current focused proof. [solve SelectAll
-    tac] applies [tac] to all subgoals. *)
-
-val solve : ?with_end_tac:unit Proofview.tactic ->
-      Goal_select.t -> int option -> unit Proofview.tactic ->
-      Proof.t -> Proof.t * bool
-
-(** Option telling if unification heuristics should be used. *)
-val use_unification_heuristics : unit -> bool
-
-val refine_by_tactic
-  :  name:Id.t
-  -> poly:bool
-  -> env -> Evd.evar_map
-  -> EConstr.types
-  -> unit Proofview.tactic
-  -> constr * Evd.evar_map
-(** A variant of the above function that handles open terms as well.
-    Caveat: all effects are purged in the returned term at the end, but other
-    evars solved by side-effects are NOT purged, so that unexpected failures may
-    occur. Ideally all code using this function should be rewritten in the
-    monad. *)
diff --git a/proofs/proof.ml b/proofs/proof.ml
index 21006349d2..731608e629 100644
--- a/proofs/proof.ml
+++ b/proofs/proof.ml
@@ -506,3 +506,107 @@ let pr_proof p =
     str "given up: " ++ pr_goal_list given_up ++
     str "]"
   )
+
+let use_unification_heuristics =
+  Goptions.declare_bool_option_and_ref
+    ~depr:false
+    ~key:["Solve";"Unification";"Constraints"]
+    ~value:true
+
+exception SuggestNoSuchGoals of int * t
+
+let solve ?with_end_tac gi info_lvl tac pr =
+    let tac = match with_end_tac with
+      | None -> tac
+      | Some etac -> Proofview.tclTHEN tac etac in
+    let tac = match info_lvl with
+      | None -> tac
+      | Some _ -> Proofview.Trace.record_info_trace tac
+    in
+    let nosuchgoal = Proofview.tclZERO (SuggestNoSuchGoals (1,pr)) in
+    let tac = let open Goal_select in match gi with
+      | SelectAlreadyFocused ->
+        let open Proofview.Notations in
+        Proofview.numgoals >>= fun n ->
+        if n == 1 then tac
+        else
+          let e = CErrors.UserError
+              (None,
+               Pp.(str "Expected a single focused goal but " ++
+                   int n ++ str " goals are focused."))
+          in
+          Proofview.tclZERO e
+
+      | SelectNth i -> Proofview.tclFOCUS ~nosuchgoal i i tac
+      | SelectList l -> Proofview.tclFOCUSLIST ~nosuchgoal l tac
+      | SelectId id -> Proofview.tclFOCUSID ~nosuchgoal id tac
+      | SelectAll -> tac
+    in
+    let tac =
+      if use_unification_heuristics () then
+        Proofview.tclTHEN tac Refine.solve_constraints
+      else tac
+    in
+    let env = Global.env () in
+    let (p,(status,info),()) = run_tactic env tac pr in
+    let env = Global.env () in
+    let sigma = Evd.from_env env in
+    let () =
+      match info_lvl with
+      | None -> ()
+      | Some i -> Feedback.msg_info (Pp.hov 0 (Proofview.Trace.pr_info env sigma ~lvl:i info))
+    in
+    (p,status)
+
+(**********************************************************************)
+(* Shortcut to build a term using tactics *)
+
+let refine_by_tactic ~name ~poly env sigma ty tac =
+  (* Save the initial side-effects to restore them afterwards. We set the
+     current set of side-effects to be empty so that we can retrieve the
+     ones created during the tactic invocation easily. *)
+  let eff = Evd.eval_side_effects sigma in
+  let sigma = Evd.drop_side_effects sigma in
+  (* Save the existing goals *)
+  let prev_future_goals = Evd.save_future_goals sigma in
+  (* Start a proof *)
+  let prf = start ~name ~poly sigma [env, ty] in
+  let (prf, _, ()) =
+    try run_tactic env tac prf
+    with Logic_monad.TacticFailure e as src ->
+      (* Catch the inner error of the monad tactic *)
+      let (_, info) = Exninfo.capture src in
+      Exninfo.iraise (e, info)
+  in
+  (* Plug back the retrieved sigma *)
+  let { goals; stack; shelf; given_up; sigma; entry } = data prf in
+  assert (stack = []);
+  let ans = match Proofview.initial_goals entry with
+  | [c, _] -> c
+  | _ -> assert false
+  in
+  let ans = EConstr.to_constr ~abort_on_undefined_evars:false sigma ans in
+  (* [neff] contains the freshly generated side-effects *)
+  let neff = Evd.eval_side_effects sigma in
+  (* Reset the old side-effects *)
+  let sigma = Evd.drop_side_effects sigma in
+  let sigma = Evd.emit_side_effects eff sigma in
+  (* Restore former goals *)
+  let sigma = Evd.restore_future_goals sigma prev_future_goals in
+  (* Push remaining goals as future_goals which is the only way we
+     have to inform the caller that there are goals to collect while
+     not being encapsulated in the monad *)
+  (* Goals produced by tactic "shelve" *)
+  let sigma = List.fold_right (Evd.declare_future_goal ~tag:Evd.ToShelve) shelf sigma in
+  (* Goals produced by tactic "give_up" *)
+  let sigma = List.fold_right (Evd.declare_future_goal ~tag:Evd.ToGiveUp) given_up sigma in
+  (* Other goals *)
+  let sigma = List.fold_right Evd.declare_future_goal goals sigma in
+  (* Get rid of the fresh side-effects by internalizing them in the term
+     itself. Note that this is unsound, because the tactic may have solved
+     other goals that were already present during its invocation, so that
+     those goals rely on effects that are not present anymore. Hopefully,
+     this hack will work in most cases. *)
+  let neff = neff.Evd.seff_private in
+  let (ans, _) = Safe_typing.inline_private_constants env ((ans, Univ.ContextSet.empty), neff) in
+  ans, sigma
diff --git a/proofs/proof.mli b/proofs/proof.mli
index 1a0b105723..0f327e2a25 100644
--- a/proofs/proof.mli
+++ b/proofs/proof.mli
@@ -207,3 +207,34 @@ end
 
 (* returns the set of all goals in the proof *)
 val all_goals : t -> Goal.Set.t
+
+(** [solve (SelectNth n) tac] applies tactic [tac] to the [n]th
+    subgoal of the current focused proof. [solve SelectAll
+    tac] applies [tac] to all subgoals. *)
+
+val solve :
+     ?with_end_tac:unit Proofview.tactic
+  -> Goal_select.t
+  -> int option
+  -> unit Proofview.tactic
+  -> t
+  -> t * bool
+
+(** Option telling if unification heuristics should be used. *)
+val use_unification_heuristics : unit -> bool
+
+val refine_by_tactic
+  :  name:Names.Id.t
+  -> poly:bool
+  -> Environ.env
+  -> Evd.evar_map
+  -> EConstr.types
+  -> unit Proofview.tactic
+  -> Constr.constr * Evd.evar_map
+(** A variant of the above function that handles open terms as well.
+    Caveat: all effects are purged in the returned term at the end, but other
+    evars solved by side-effects are NOT purged, so that unexpected failures may
+    occur. Ideally all code using this function should be rewritten in the
+    monad. *)
+
+exception SuggestNoSuchGoals of int * t
diff --git a/proofs/proof_bullet.ml b/proofs/proof_bullet.ml
index f619bc86a1..41cb7399da 100644
--- a/proofs/proof_bullet.ml
+++ b/proofs/proof_bullet.ml
@@ -191,11 +191,8 @@ let put p b =
 let suggest p =
   (current_behavior ()).suggest p
 
-(* Better printing for bullet exceptions *)
-exception SuggestNoSuchGoals of int * Proof.t
-
 let _ = CErrors.register_handler begin function
-    | SuggestNoSuchGoals(n,proof) ->
+    | Proof.SuggestNoSuchGoals(n,proof) ->
       let suffix = suggest proof in
       Some (Pp.(str "No such " ++ str (CString.plural n "goal") ++ str "." ++
                 pr_non_empty_arg (fun x -> x) suffix))
diff --git a/proofs/proof_bullet.mli b/proofs/proof_bullet.mli
index 687781361c..f15b7824ff 100644
--- a/proofs/proof_bullet.mli
+++ b/proofs/proof_bullet.mli
@@ -44,5 +44,3 @@ val register_behavior : behavior -> unit
      *)
 val put : Proof.t -> t -> Proof.t
 val suggest : Proof.t -> Pp.t
-
-exception SuggestNoSuchGoals of int * Proof.t
diff --git a/proofs/proofs.mllib b/proofs/proofs.mllib
index 91e1ee22aa..756fef0511 100644
--- a/proofs/proofs.mllib
+++ b/proofs/proofs.mllib
@@ -6,7 +6,6 @@ Proof
 Logic
 Goal_select
 Proof_bullet
-Pfedit
 Refiner
 Tacmach
 Clenv
diff --git a/stm/stm.ml b/stm/stm.ml
index 076810c750..8dcd7bbfd5 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -2310,7 +2310,7 @@ let known_state ~doc ?(redefine_qed=false) ~cache id =
                Option.iter PG_compat.unfreeze lemmas;
                PG_compat.with_current_proof (fun _ p ->
                  feedback ~id:id Feedback.AddedAxiom;
-                 fst (Pfedit.solve Goal_select.SelectAll None tac p), ());
+                 fst (Proof.solve Goal_select.SelectAll None tac p), ());
                (* STATE SPEC:
                 * - start: Modifies the input state adding a proof.
                 * - end  : maybe after recovery command.
diff --git a/tactics/declare.ml b/tactics/declare.ml
index e1ddf262a0..6945f13fc3 100644
--- a/tactics/declare.ml
+++ b/tactics/declare.ml
@@ -779,7 +779,7 @@ let update_global_env =
 
 let next = let n = ref 0 in fun () -> incr n; !n
 
-let by tac = map_fold_proof (Pfedit.solve (Goal_select.SelectNth 1) None tac)
+let by tac = map_fold_proof (Proof.solve (Goal_select.SelectNth 1) None tac)
 
 let build_constant_by_tactic ~name ?(opaque=Transparent) ~uctx ~sign ~poly typ tac =
   let evd = Evd.from_ctx uctx in
diff --git a/user-contrib/Ltac2/tac2core.ml b/user-contrib/Ltac2/tac2core.ml
index 72df4d75c8..2102cd1172 100644
--- a/user-contrib/Ltac2/tac2core.ml
+++ b/user-contrib/Ltac2/tac2core.ml
@@ -1290,7 +1290,7 @@ let () =
     let ist = Tac2interp.get_env ist in
     let tac = Proofview.tclIGNORE (Tac2interp.interp ist tac) in
     let name, poly = Id.of_string "ltac2", poly in
-    let c, sigma = Pfedit.refine_by_tactic ~name ~poly env sigma concl tac in
+    let c, sigma = Proof.refine_by_tactic ~name ~poly env sigma concl tac in
     (EConstr.of_constr c, sigma)
   in
   GlobEnv.register_constr_interp0 wit_ltac2_constr interp
diff --git a/user-contrib/Ltac2/tac2entries.ml b/user-contrib/Ltac2/tac2entries.ml
index b84fd0b6d9..136ea8b7e0 100644
--- a/user-contrib/Ltac2/tac2entries.ml
+++ b/user-contrib/Ltac2/tac2entries.ml
@@ -902,7 +902,7 @@ let solve ~pstate default tac =
   let pstate, status = Declare.map_fold_proof_endline begin fun etac p ->
     let with_end_tac = if default then Some etac else None in
     let g = Goal_select.get_default_goal_selector () in
-    let (p, status) = Pfedit.solve g None tac ?with_end_tac p in
+    let (p, status) = Proof.solve g None tac ?with_end_tac p in
     (* in case a strict subtree was completed,
        go back to the top of the prooftree *)
     let p = Proof.maximal_unfocus Vernacentries.command_focus p in