index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
tactics
/
rewrite.ml
Commit message (
Expand
)
Author
Age
*
Dedicated inductive for return values of rewrite strategies.
Pierre-Marie Pédrot
2013-12-16
*
Writing [cut] tactic using the new monad.
Pierre-Marie Pédrot
2013-12-02
*
Adding generic solvers to term holes. For now, no resolution mechanism nor
Pierre-Marie Pédrot
2013-11-27
*
Porting Tactics.assumption to the new engine.
ppedrot
2013-11-08
*
Tachmach.New is now in Proofview.Goal.enter style.
aspiwack
2013-11-02
*
More Proofview.Goal.enter.
aspiwack
2013-11-02
*
The tactic [admit] exits with the "unsafe" status.
aspiwack
2013-11-02
*
Clean-up: removed redundant notations (>>-) and (>>--) from Proofview.Notations.
aspiwack
2013-11-02
*
Getting rid of Goal.here, and all the related exceptions and combinators.
aspiwack
2013-11-02
*
Makes the new Proofview.tactic the basic type of Ltac.
aspiwack
2013-11-02
*
Conv_orable made functional and part of pre_env
gareuselesinge
2013-10-31
*
More monomorphic List.mem + List.assoc + ...
letouzey
2013-10-24
*
declaration_hooks use Ephemeron
gareuselesinge
2013-10-18
*
Moving side effects into evar_map. There was no reason to keep another
ppedrot
2013-10-05
*
Fixing potential evar leak in Rewrite, and removing dead code.
ppedrot
2013-10-05
*
Made rewrite tactic strategies pure. They were using quite uglily
ppedrot
2013-09-28
*
Splitting Rewrite into a code part and a CAMLP4-dependent one.
ppedrot
2013-09-26