coq - The formal proof system

Age	Commit message (Expand)	Author
2014-08-05	Experimentally adding an option for automatically erasing an	Hugo Herbelin
2014-08-05	Adding a syntax "enough" for the variant of "assert" with the order of	Hugo Herbelin
2014-08-05	A new step in the new "standard" naming policy for propositional hypotheses	Hugo Herbelin
2014-08-01	CHANGES: [>…].	Arnaud Spiwack
2014-08-01	CHANGES: [numgoals] and [guard].	Arnaud Spiwack
2014-07-31	Making the error message about bullets more precise.	Pierre Courtieu
2014-07-29	CHANGES: untyped terms in tactics	Arnaud Spiwack
2014-07-25	CHANGES: cycle and swap.	Arnaud Spiwack
2014-07-25	CHANGES: yellow in Coqide.	Arnaud Spiwack
2014-07-25	CHANGE: add Derive.	Arnaud Spiwack
2014-07-25	CHANGE: document the features of the new tactic engine.	Arnaud Spiwack
2014-07-21	Documenting the changes of Locate semantics.	Pierre-Marie Pédrot
2014-07-21	Documenting the need of the "DECLARE PLUGIN" statement.	Pierre-Marie Pédrot
2014-07-21	Documenting the change of semantics of the "constructor" tactic.	Pierre-Marie Pédrot
2014-07-13	Mentioning the incompatibility due to fixing bug #2996 (see #3418).	Hugo Herbelin
2014-07-13	Adding a "time" tactical for benchmarking purposes. In case the tactic	Hugo Herbelin
2014-06-30	Synchronized names from the "as" clause with the skeleton of the	Hugo Herbelin
2014-06-28	Updating CHANGES w.r.t. opacity in type inference + layout of file.	Hugo Herbelin
2014-06-23	Add some compatibility notes on the changes to [change] and unification in ge...	Matthieu Sozeau
2014-06-01	Use of "H"-based names for propositional hypotheses obtained by	Hugo Herbelin
2014-05-31	More on injection over a projectable "existT". - Fixing syntax "injection ......	Hugo Herbelin
2014-05-18	Restored old behavior of injection on proofs by default.	Maxime Dénès
2014-05-09	More documentation of new features in CHANGE.	Pierre-Marie Pédrot
2014-05-08	Simplification and improvement of "subst x" in such a way that it	Hugo Herbelin
2014-05-06	This commit adds full universe polymorphism and fast projections to Coq.	Matthieu Sozeau
2014-04-30	Document changes on injection.	Maxime Dénès
2014-04-09	Revert "Revert part of eba6b75 as coq_makefile ignores -I if it overlaps with...	Pierre Boutillier
2014-04-08	Add an option -Q (tentative name).	Guillaume Melquiond
2014-04-07	Revert part of eba6b75 as coq_makefile ignores -I if it overlaps with -R. (Fi...	Guillaume Melquiond
2014-04-06	Change handling of loadpath and mlpath.	Guillaume Melquiond
2014-01-30	Coqmktop without Sys.command, changes in ./configure -*byteflags options	Pierre Letouzey
2014-01-25	More in CHANGES.	Pierre-Marie Pédrot
2014-01-10	Omega: avoiding distinct proof-terms on repeated identical runs	Pierre Letouzey
2013-12-11	Documenting the tactic-in-term construction.	Pierre-Marie Pédrot
2013-08-22	Change in vo format : digest aren't Marshalled anymore	letouzey
2013-07-09	Revising r16550 about providing intro patterns for applying injection:	herbelin
2013-06-06	Document changes and add missing documentation for Program options.	msozeau
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-29	Documenting the "appcontext" by default.	ppedrot
2013-05-14	"change ... in ..." and "simpl ... in ..." now consider nested	herbelin
2013-05-05	Reporting the change on matching partial applications in patterns of	herbelin
2013-04-17	Renaming SearchAbout into Search and Search into SearchHead.	herbelin
2013-03-21	Using hnf instead of "intro H" for forcing reduction to a product.	herbelin
2013-03-21	Fixing an old pecularity of "red": head betaiota redexes are now	herbelin
2013-03-11	Allowing (Co)Fixpoint to be defined local and Let-style.	ppedrot
2013-03-11	Added a Local Definition vernacular command. This type of definition	ppedrot
2013-02-17	Displaying environment and unfolding aliases in "cannot_unify"	herbelin
2012-12-04	Revised the strategy for automatic insertion of spaces when printing	herbelin
2012-08-23	CHANGES: document the end of states/initial.coq and coqtop.opt	letouzey