From d0da8a75cd1d600afa68da5e995d39a415234c2d Mon Sep 17 00:00:00 2001
From: Arnaud Spiwack
Date: Thu, 16 Oct 2014 17:13:38 +0200
Subject: Refactoring proofview: make the definition of the logic monad
 polymorphic.

Makes the monad more flexible as it will be easier to add new components to the concrete state of the tactic monad.

The Proofview module is also organised in a more abstract way with dedicated submodules to access various parts of the state or writer.
---
 proofs/proofview.mli | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'proofs/proofview.mli')

diff --git a/proofs/proofview.mli b/proofs/proofview.mli
index d822f933be..45a0c94846 100644
--- a/proofs/proofview.mli
+++ b/proofs/proofview.mli
@@ -133,7 +133,7 @@ type 'a case =
    case it is [false]. *)
 val apply : Environ.env -> 'a tactic -> proofview -> 'a
                                                    * proofview
-                                                   * (bool*(Goal.goal list*Goal.goal list))
+                                                   * (bool*Goal.goal list*Goal.goal list)
 
 (*** tacticals ***)
 
-- 
cgit v1.2.3