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/proof.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'proofs/proof.ml')

diff --git a/proofs/proof.ml b/proofs/proof.ml
index 53b73097f9..8d43513f26 100644
--- a/proofs/proof.ml
+++ b/proofs/proof.ml
@@ -318,7 +318,7 @@ let initial_goals p = Proofview.initial_goals p.entry
 
 let run_tactic env tac pr =
   let sp = pr.proofview in
-  let (_,tacticced_proofview,(status,(to_shelve,give_up))) = Proofview.apply env tac sp in
+  let (_,tacticced_proofview,(status,to_shelve,give_up)) = Proofview.apply env tac sp in
   let shelf =
     Proofview.in_proofview tacticced_proofview begin fun sigma ->
       let pre_shelf = pr.shelf@(Evd.future_goals sigma)@to_shelve in
-- 
cgit v1.2.3