From 038819807ba7cab0bc451dfd1f6772eae110826b Mon Sep 17 00:00:00 2001
From: Arnaud Spiwack
Date: Tue, 21 Oct 2014 16:50:47 +0200
Subject: Split [Proofview] into a file where the basic operations on the state
 are defined and the file providing the primitives.

The datatypes are defined in [Proofview_monad], previous [Proofview_monad] is now called [Logic_monad] since it is more generic since the refactoring.
---
 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 e5177e4bd8..443ec5aaed 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -2154,7 +2154,7 @@ let _ =
       let prf = Proof.start sigma [env, ty] in
       let (prf, _) =
         try Proof.run_tactic env tac prf
-        with Proofview_monad.TacticFailure e as src ->
+        with Logic_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 83a3f2604e..697b09309e 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -4103,7 +4103,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 Proofview_monad.TacticFailure e as src ->
+    with Logic_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