coq - The formal proof system

Age	Commit message (Expand)	Author
2013-11-02	Made Proofview.Goal.hyps a named_context.	aspiwack
2013-11-02	Refine does beta-reductions.	aspiwack
2013-11-02	Adds a tactical once.	aspiwack
2013-11-02	Corrects the semantics of the "+" tactical.	aspiwack
2013-11-02	Less use of the list-based interface for goal-bound tactics.	aspiwack
2013-11-02	Tachmach.New is now in Proofview.Goal.enter style.	aspiwack
2013-11-02	More Proofview.Goal.enter.	aspiwack
2013-11-02	Added the tactical "tac1 + tac2".	aspiwack
2013-11-02	Try to remove intermediate allocations when dealing with goal-specific tactics.	aspiwack
2013-11-02	Various rewriting, mostly for speed purposes.	aspiwack
2013-11-02	Fix behaviour of the refine tactic with respect to evars in types.	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	Removed spurious try/with in Proofview.Notation.(>>=) and (>>==).	aspiwack
2013-11-02	Clean up a warning.	aspiwack
2013-11-02	The tactic [admit] exits with the "unsafe" status.	aspiwack
2013-11-02	Cleanup of comments.	aspiwack
2013-11-02	A whole new implemenation of the refine tactic.	aspiwack
2013-11-02	A newly introduced variable inside a named context is no longer α-renamed.	aspiwack
2013-11-02	Clean-up: removed redundant notations (>>-) and (>>--) from Proofview.Notations.	aspiwack
2013-11-02	Bases tactics on an IO monad.	aspiwack
2013-11-02	Getting rid of Goal.here, and all the related exceptions and combinators.	aspiwack
2013-11-02	Uses Proofview.tclEXTEND more sparingly.	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-28	Evar leak in "absurd" tactic.	ppedrot
2013-10-24	More monomorphic List.mem + List.assoc + ...	letouzey
2013-10-23	cList: set-as-list functions are now with an explicit comparison	letouzey
2013-10-23	Tacintern: avoid a match (fst (List.hd ...))	letouzey
2013-10-18	declaration_hooks use Ephemeron	gareuselesinge
2013-10-06	Removing uses of Evar.add in class-related functions.	ppedrot
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-10-05	Fixing potential evar leak in Equality.	ppedrot
2013-10-04	Splitting Class_tactics between code and CAMLP4/5 declarations.	ppedrot
2013-09-28	Made rewrite tactic strategies pure. They were using quite uglily	ppedrot
2013-09-27	Removing a bunch of generic equalities.	ppedrot
2013-09-26	Opacifying the type of strategies.	ppedrot
2013-09-26	Splitting Rewrite into a code part and a CAMLP4-dependent one.	ppedrot
2013-09-19	Get rid of the uses of deprecated OCaml elements (still remaining compatible ...	xclerc
2013-09-18	At least made the evar type opaque! There are still 5 remaining unsafe	ppedrot
2013-09-18	Removing unused code from Term_dnet.	ppedrot
2013-09-05	Optimizing some evar_maps manipulation. In particular, using a [map] instead	ppedrot
2013-09-03	Some cleanup in Auto	ppedrot
2013-08-28	Removing some lone List.assoc & List.mem in lib.	ppedrot
2013-08-25	Actually using the domain function for maps.	ppedrot
2013-08-22	Less "Coq" strings everywhere	letouzey
2013-08-08	get rid of closures in global/proof state	gareuselesinge
2013-08-08	Vernac classification streamlined (handles VERNAC EXTEND)	gareuselesinge
2013-08-08	State Transaction Machine	gareuselesinge