coq - The formal proof system

Age	Commit message (Expand)	Author
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	Removed spurious try/with in Proofview.Notation.(>>=) and (>>==).	aspiwack
2013-11-02	Clean up a warning.	aspiwack
2013-11-02	Cleanup of comments.	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-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-05	Moving side effects into evar_map. There was no reason to keep another	ppedrot
2013-10-05	Fixing potential evar leak in Equality.	ppedrot
2013-09-27	Removing a bunch of generic equalities.	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-08-08	State Transaction Machine	gareuselesinge
2013-07-10	Continuing r16621 on injection intro-patterns:	herbelin
2013-07-09	Revising r16550 about providing intro patterns for applying injection:	herbelin
2013-06-02	Making the behavior of "injection ... as ..." more natural:	herbelin
2013-06-02	Now interpreting introduction patterns [x1 .. xn] and (x1,..,xn) as an	herbelin
2013-05-12	Use the Hook module here and there.	ppedrot
2013-04-29	Merging Context and Sign.	ppedrot
2013-04-29	Splitting Term into five unrelated interfaces:	ppedrot
2013-04-10	Equality: avoid some unprotected List.nth (fix #2837)	letouzey
2013-03-13	Restrict (try...with...) to avoid catching critical exn (part 10)	letouzey
2013-03-12	Equality: avoid an anomaly about inj_pair2_eq_dec	letouzey
2013-01-28	Actually adding backtrace handling.	ppedrot
2013-01-28	Uniformization of the "anomaly" command.	ppedrot
2012-12-18	Modulification of Label	ppedrot
2012-12-18	Fixed a little inefficiency of "set/destruct" over a pattern. Now	herbelin
2012-12-14	Modulification of identifier	ppedrot
2012-12-14	Moved Intset and Intmap to Int namespace.	ppedrot
2012-11-25	Monomorphization (tactics)	ppedrot
2012-11-08	Monomorphized a lot of equalities over OCaml integers, thanks to	ppedrot
2012-10-04	Revert r15851 "En cours pour bug 2836".	herbelin
2012-10-04	En cours pour bug 2836	herbelin
2012-10-02	Remove some more "open" and dead code thanks to OCaml4 warnings	letouzey
2012-09-18	Cleaning interface of Util.	ppedrot
2012-09-17	More cleaning on Utils and CList. Some parts of the code being	ppedrot
2012-09-15	Some documentation and cleaning of CList and Util interfaces.	ppedrot
2012-09-14	Moving Utils.list_* to a proper CList module, which includes stdlib	ppedrot
2012-09-14	This patch removes unused "open" (automatically generated from	regisgia
2012-08-08	Updating headers.	herbelin
2012-06-22	Added an indirection with respect to Loc in Compat. As many [open Compat]	ppedrot
2012-05-29	global_reference migrated from Libnames to new Globnames, less deps in gramma...	letouzey
2012-05-29	Tacexpr as a mli-only, the few functions there are now in Tacops	letouzey
2012-05-29	locus.mli for occurrences+clauses, misctypes.mli for various little things	letouzey
2012-03-02	Noise for nothing	pboutill
2011-12-17	Added a flag to control the use of typing when instantiating applied	herbelin