aboutsummaryrefslogtreecommitdiff
path: root/kernel/type_errors.ml
diff options
context:
space:
mode:
authorPierre-Marie Pédrot2014-07-23 20:06:27 +0200
committerPierre-Marie Pédrot2014-07-24 15:06:09 +0200
commitfb4187a6d475719bada0a7fe1b7902a36e06d658 (patch)
tree4b628f26dc1911007baa997f5e371f0340cb8ec1 /kernel/type_errors.ml
parenta435938aa7d1c94c40ddb17627cfaa2fb9f45f0f (diff)
New implementation of the tactic monad.
The new implementation is made of two layers: a iolist, which is essentially a stream without memoization, and above this a state monad. The previous design of the extracted monad kept three distinct but similar monad transformers: a stateT, a writerT and a readerT. We take advantage of this similarity to pack those three transformers into only one state monad. This makes the code cleaner and hopefully more efficient.
Diffstat (limited to 'kernel/type_errors.ml')
0 files changed, 0 insertions, 0 deletions