coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Use of "H"-based names for propositional hypotheses obtained by	Hugo Herbelin	2014-06-01
*	More on injection over a projectable "existT". - Fixing syntax "injection ......	Hugo Herbelin	2014-05-31
*	Restored old behavior of injection on proofs by default.	Maxime Dénès	2014-05-18
*	More documentation of new features in CHANGE.	Pierre-Marie Pédrot	2014-05-09
*	Simplification and improvement of "subst x" in such a way that it	Hugo Herbelin	2014-05-08
*	This commit adds full universe polymorphism and fast projections to Coq.	Matthieu Sozeau	2014-05-06
*	Document changes on injection.	Maxime Dénès	2014-04-30
*	Revert "Revert part of eba6b75 as coq_makefile ignores -I if it overlaps with...	Pierre Boutillier	2014-04-09
*	Add an option -Q (tentative name).	Guillaume Melquiond	2014-04-08
*	Revert part of eba6b75 as coq_makefile ignores -I if it overlaps with -R. (Fi...	Guillaume Melquiond	2014-04-07
*	Change handling of loadpath and mlpath.	Guillaume Melquiond	2014-04-06
*	Coqmktop without Sys.command, changes in ./configure -*byteflags options	Pierre Letouzey	2014-01-30
*	More in CHANGES.	Pierre-Marie Pédrot	2014-01-25
*	Omega: avoiding distinct proof-terms on repeated identical runs	Pierre Letouzey	2014-01-10
*	Documenting the tactic-in-term construction.	Pierre-Marie Pédrot	2013-12-11
*	Change in vo format : digest aren't Marshalled anymore	letouzey	2013-08-22
*	Revising r16550 about providing intro patterns for applying injection:	herbelin	2013-07-09
*	Document changes and add missing documentation for Program options.	msozeau	2013-06-06
*	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-06-02
*	Documenting the "appcontext" by default.	ppedrot	2013-05-29
*	"change ... in ..." and "simpl ... in ..." now consider nested	herbelin	2013-05-14
*	Reporting the change on matching partial applications in patterns of	herbelin	2013-05-05
*	Renaming SearchAbout into Search and Search into SearchHead.	herbelin	2013-04-17
*	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-21
*	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-03-11
*	Displaying environment and unfolding aliases in "cannot_unify"	herbelin	2013-02-17
*	Revised the strategy for automatic insertion of spaces when printing	herbelin	2012-12-04
*	CHANGES: document the end of states/initial.coq and coqtop.opt	letouzey	2012-08-23
*	Added support for option Local (at module level) in Tactic Notation.	herbelin	2012-08-11
*	Some changes in CHANGES.	herbelin	2012-08-11
*	Cleaning CHANGES consistently with v8.4. Documenting COMPATIBILITY.	herbelin	2012-08-08
*	Document the command Add/Remove Search Blacklist	letouzey	2012-08-03
*	re-sync CHANGES with 8.4	letouzey	2012-08-03
*	The tactic remember now accepts a final eqn:H option (grant wish #2489)	letouzey	2012-07-09
*	induction/destruct : nicer syntax for generating equations (solves #2741)	letouzey	2012-07-09
*	Quick update to CHANGES, mention especially the new parsing of ->	letouzey	2012-07-05
*	CHANGES: mention the end of induction principles for records	letouzey	2012-06-05
*	Some documentation of recent changes concerning interfaces	letouzey	2012-05-29
*	CHANGES: fix a typo + an entry in the wrong section	letouzey	2012-05-23
*	Intuition: temporary(?) restore the unconditional unfolding of not	letouzey	2012-05-15
*	Remove the Dp plugin.	gmelquio	2012-04-17
*	Fixing tauto "special" behavior on singleton types w/ 2 parameters (bug #2680).	herbelin	2012-04-15
*	Update CHANGES	herbelin	2012-04-15
*	MSetRBT : implementation of MSets via Red-Black trees	letouzey	2012-04-13
*	CHANGES: adapt after backport of some features to 8.4	letouzey	2012-04-12
*	info_trivial, info_auto, info_eauto, and debug (trivial\|auto)	letouzey	2012-03-30
*	Slight change in the semantics of arguments scopes: scopes can no	herbelin	2012-03-26