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

1 files changed, 31 insertions, 0 deletions

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