aboutsummaryrefslogtreecommitdiff
path: root/kernel/nativelib.ml
diff options
context:
space:
mode:
authorPierre-Marie Pédrot2015-04-19 12:25:50 +0200
committerPierre-Marie Pédrot2015-05-06 15:35:16 +0200
commit87c8236de9a8141ea6925cf4390a971f0a941ae8 (patch)
treecb4e363228f99a1e303402dabb41c0de2d29fc53 /kernel/nativelib.ml
parent34e6a7149a69791cc736bdd9b2b909be9f21ec8f (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 'kernel/nativelib.ml')
0 files changed, 0 insertions, 0 deletions