From 87c8236de9a8141ea6925cf4390a971f0a941ae8 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 19 Apr 2015 12:25:50 +0200
Subject: Exposing the minimal amount of internal of the Logic monad in order
 to allow reusability of the implementation throughout the Coq codebase.

We effectively feature a generalized version of the logical monad where the
input state, the output state and the inner exception can be arbitrarily chosen.
This will allow for more efficient implementations of close variants of the
monad.
---
 proofs/proofview.ml  | 2 +-
 proofs/proofview.mli | 9 +++++++++
 2 files changed, 10 insertions(+), 1 deletion(-)

(limited to 'proofs')

diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index 6e653806b7..64ea5aea01 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -887,7 +887,7 @@ module Unsafe = struct
 
 end
 
-
+module UnsafeRepr = Proof.Unsafe
 
 (** {7 Notations} *)
 
diff --git a/proofs/proofview.mli b/proofs/proofview.mli
index 5a9e7f39f0..98e1477ff1 100644
--- a/proofs/proofview.mli
+++ b/proofs/proofview.mli
@@ -405,6 +405,15 @@ module Unsafe : sig
   val mark_as_goal : proofview -> Evar.t -> proofview
 end
 
+(** This module gives access to the innards of the monad. Its use is
+    restricted to very specific cases. *)
+module UnsafeRepr :
+sig
+  type state = Proofview_monad.Logical.Unsafe.state
+  val repr : 'a tactic -> ('a, state, state, iexn) Logic_monad.BackState.t
+  val make : ('a, state, state, iexn) Logic_monad.BackState.t -> 'a tactic
+end
+
 (** {7 Notations} *)
 
 module Notations : sig
-- 
cgit v1.2.3