diff options
author | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-04-19 12:25:50 +0200 |
---|---|---|
committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-05-06 15:35:16 +0200 |
commit | 87c8236de9a8141ea6925cf4390a971f0a941ae8 (patch) | |
tree | cb4e363228f99a1e303402dabb41c0de2d29fc53 /proofs/proofview.ml | |
parent | 34e6a7149a69791cc736bdd9b2b909be9f21ec8f (diff) |
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.
Diffstat (limited to 'proofs/proofview.ml')
-rw-r--r-- | proofs/proofview.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/proofs/proofview.ml b/proofs/proofview.ml index 6e653806b..64ea5aea0 100644 --- a/proofs/proofview.ml +++ b/proofs/proofview.ml @@ -887,7 +887,7 @@ module Unsafe = struct end - +module UnsafeRepr = Proof.Unsafe (** {7 Notations} *) |