index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
bootstrap
Age
Commit message (
Expand
)
Author
2013-11-02
Cleanup of comments in bootstrap/Monads.v
aspiwack
2013-11-02
Adds a tactic give_up.
aspiwack
2013-11-02
Adds a shelve tactic.
aspiwack
2013-11-02
bootstrap/Monad.v: implements the writer monad in continuation passing style.
aspiwack
2013-11-02
bootstrap/Monad.v: implements the environment monad in continuation passing s...
aspiwack
2013-11-02
Factors the lifting of environment and writer monads in bootstrap/Monad.v
aspiwack
2013-11-02
A dedicated view type for Proofview_gen.split.
aspiwack
2013-11-02
Typos in a comment.
aspiwack
2013-11-02
bootstrap/Monads.v: A more efficient split.
aspiwack
2013-11-02
State monad implemented in CPS.
aspiwack
2013-11-02
A more principled split.
aspiwack
2013-11-02
Set an extraction flag for inling let-s in Monad.v.
aspiwack
2013-11-02
Various rewriting, mostly for speed purposes.
aspiwack
2013-11-02
Optimisation of partial applications in the tactic monad.
aspiwack
2013-11-02
Makes the Ltac debugger usable again.
aspiwack
2013-11-02
Replaced monads.ml by an essentially equivalent proofview_gen.ml generated by...
aspiwack
