[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.

7 files changed, 136 insertions, 163 deletions

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