index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
proofs
/
proofview_monad.mli
Commit message (
Expand
)
Author
Age
*
Refactoring proofview: make the definition of the logic monad polymorphic.
Arnaud Spiwack
2014-10-16
*
Adding a tclUPDATE_ENV primitive and using it in in tclABSTRACT.
Pierre-Marie Pédrot
2014-09-04
*
Revert "Tactics: [tclENV] is now sensitive to [Proofview.Goal.enter]."
Pierre-Marie Pédrot
2014-09-04
*
Adding a [make] primitive to the NonLogical monad.
Pierre-Marie Pédrot
2014-08-05
*
Tactics: [tclENV] is now sensitive to [Proofview.Goal.enter].
Arnaud Spiwack
2014-08-05
*
Some comments in the interface of Proofview_monad.
Arnaud Spiwack
2014-08-04
*
Cleaning of the new implementation of the tactic monad.
Arnaud Spiwack
2014-08-04
*
Adding a tclBREAK primitive to the tactic monad.
Pierre-Marie Pédrot
2014-07-28
*
Adding a tail-rec tclONCE.
Pierre-Marie Pédrot
2014-07-24
*
Revert "time tac" (committed by mistake).
Hugo Herbelin
2014-07-07
*
time tac
Hugo Herbelin
2014-07-07
*
Adding a [map] primitive to the tactic monad. Hopefully this should be
Pierre-Marie Pédrot
2014-04-20
*
Transfering the initial goals from the proofview to the proof object.
Pierre-Marie Pédrot
2014-04-07
*
Adding an [modify] function to the tactic monad. It allows to modify
Pierre-Marie Pédrot
2014-04-06
*
Adds a tactic give_up.
aspiwack
2013-11-02
*
Adds a shelve tactic.
aspiwack
2013-11-02
*
A dedicated view type for Proofview_gen.split.
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
2013-11-02