From 94a759be56074ac66c5c96b0cc7722b395c4cf40 Mon Sep 17 00:00:00 2001
From: Arnaud Spiwack
Date: Mon, 4 Aug 2014 15:44:19 +0200
Subject: Cleaning of the new implementation of the tactic monad.

* Add comments in the code (mostly imported from Monad.v)
* Inline duplicated module
* Clean up some artifacts due to the extracted code.
* [NonLogical.new_ref] -> [NonLogical.ref] (I don't even remember why I chose this name originally)
* Remove the now superfluous [Proof_errors] module (which was used to define exceptions to be used in the extracted code).
* Remove Monad.v
---
 tactics/tacinterp.ml | 2 +-
 tactics/tactics.ml   | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

(limited to 'tactics')

diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index cca26bf055..826846f906 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -2120,7 +2120,7 @@ let _ =
       let prf = Proof.start sigma [env, ty] in
       let (prf, _) =
         try Proof.run_tactic env tac prf
-        with Proof_errors.TacticFailure e as src ->
+        with Proofview_monad.TacticFailure e as src ->
           (** Catch the inner error of the monad tactic *)
           let src = Errors.push src in
           let e = Backtrace.app_backtrace ~src ~dst:e in
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 07ac0ba9f2..3b1cf65755 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -3748,7 +3748,7 @@ let abstract_subproof id gk tac =
   let ectx = Evd.evar_universe_context evd in
   let (const, safe, ectx) =
     try Pfedit.build_constant_by_tactic ~goal_kind:gk id ectx secsign concl solve_tac
-    with Proof_errors.TacticFailure e as src ->
+    with Proofview_monad.TacticFailure e as src ->
     (* if the tactic [tac] fails, it reports a [TacticFailure e],
        which is an error irrelevant to the proof system (in fact it
        means that [e] comes from [tac] failing to yield enough
-- 
cgit v1.2.3