Allow run_tactic to return a value, remove hack from ltac2

4 files changed, 8 insertions, 8 deletions

diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index 4f36354f79..52e15f466f 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -98,7 +98,7 @@ let solve ?with_end_tac gi info_lvl tac pr =
       else tac
     in
     let env = Global.env () in
-    let (p,(status,info)) = Proof.run_tactic env tac pr 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 () =
@@ -161,7 +161,7 @@ let refine_by_tactic ~name ~poly env sigma ty tac =
   let prev_future_goals = save_future_goals sigma in
   (* Start a proof *)
   let prf = Proof.start ~name ~poly sigma [env, ty] in
-  let (prf, _) =
+  let (prf, _, ()) =
     try Proof.run_tactic env tac prf
     with Logic_monad.TacticFailure e as src ->
       (* Catch the inner error of the monad tactic *)
diff --git a/proofs/proof.ml b/proofs/proof.ml
index 778d98b2cd..ce7354aa62 100644
--- a/proofs/proof.ml
+++ b/proofs/proof.ml
@@ -372,7 +372,7 @@ let run_tactic env tac pr =
   let sp = pr.proofview in
   let undef sigma l = List.filter (fun g -> Evd.is_undefined sigma g) l in
   let tac =
-    tac >>= fun () ->
+    tac >>= fun result ->
     Proofview.tclEVARMAP >>= fun sigma ->
     (* Already solved goals are not to be counted as shelved. Nor are
       they to be marked as unresolvable. *)
@@ -383,10 +383,10 @@ let run_tactic env tac pr =
       CErrors.anomaly Pp.(str "Evars generated outside of proof engine (e.g. V82, clear, ...) are not supposed to be explicitly given up.");
     let sigma = Proofview.Unsafe.mark_as_goals sigma retrieved in
     Proofview.Unsafe.tclEVARS sigma >>= fun () ->
-    Proofview.tclUNIT retrieved
+    Proofview.tclUNIT (result,retrieved)
   in
   let { name; poly } = pr in
-  let (retrieved,proofview,(status,to_shelve,give_up),info_trace) =
+  let ((result,retrieved),proofview,(status,to_shelve,give_up),info_trace) =
     Proofview.apply ~name ~poly env tac sp
   in
   let sigma = Proofview.return proofview in
@@ -400,7 +400,7 @@ let run_tactic env tac pr =
   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)
+  { pr with proofview ; shelf ; given_up },(status,info_trace),result
 
 (*** Commands ***)
 
diff --git a/proofs/proof.mli b/proofs/proof.mli
index 1f4748141a..248b9d921e 100644
--- a/proofs/proof.mli
+++ b/proofs/proof.mli
@@ -172,7 +172,7 @@ val no_focused_goal : t -> bool
    used. In which case it is [false]. *)
 val run_tactic
   :  Environ.env
-  -> unit Proofview.tactic -> t -> t * (bool*Proofview_monad.Info.tree)
+  -> 'a Proofview.tactic -> t -> t * (bool*Proofview_monad.Info.tree) * 'a
 
 val maximal_unfocus : 'a focus_kind -> t -> t
 
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index 08b98d702a..40ae4acc88 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -345,6 +345,6 @@ let update_global_env (pf : t) =
   with_current_proof (fun _ p ->
      Proof.in_proof p (fun sigma ->
        let tac = Proofview.Unsafe.tclEVARS (Evd.update_sigma_env sigma (Global.env ())) in
-       let (p,(status,info)) = Proof.run_tactic (Global.env ()) tac p in
+       let (p,(status,info),()) = Proof.run_tactic (Global.env ()) tac p in
          (p, ()))) pf
   in res