coq - The formal proof system

Age	Commit message (Expand)	Author
2013-12-02	Writing [cut] tactic using the new monad.	Pierre-Marie Pédrot
2013-11-27	Adding generic solvers to term holes. For now, no resolution mechanism nor	Pierre-Marie Pédrot
2013-11-08	Porting Tactics.assumption to the new engine.	ppedrot
2013-11-02	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-10-31	Conv_orable made functional and part of pre_env	gareuselesinge
2013-10-24	More monomorphic List.mem + List.assoc + ...	letouzey
2013-10-18	declaration_hooks use Ephemeron	gareuselesinge
2013-10-05	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-09-28	Made rewrite tactic strategies pure. They were using quite uglily	ppedrot
2013-09-26	Splitting Rewrite into a code part and a CAMLP4-dependent one.	ppedrot