coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Documenting the Shrink Abstract option.	Pierre-Marie Pédrot	2015-08-22
*	Granting Jason's request for an ad hoc compatibility option on	Hugo Herbelin	2015-08-02
*	Documenting change of behavior of apply when the lemma is a tuple and	Hugo Herbelin	2015-08-02
*	Rewording about how to upgrade on failing calls to constructor.	Hugo Herbelin	2015-07-10
*	CHANGES: grammatical correction, suggested by Jason Gross on Bugzilla.	Maxime Dénès	2015-07-10
*	More precise rewording about asymmetric patterns.	Hugo Herbelin	2015-07-05
*	Introduction of a "Undelimit Scope" command, undoing "Delimit Scope"	Lionel Rieg	2015-06-26
*	Fixed CHANGES to reflect -color option.	Pierre Courtieu	2015-05-18
*	Adding an option -w to control Coq warning output.	Pierre-Marie Pédrot	2015-05-14
*	Safer typing primitives.	Pierre-Marie Pédrot	2015-05-13
*	Documenting the Loose Hint Behavior flag.	Pierre-Marie Pédrot	2015-05-13
*	Adding a flag "Set Regular Subst Tactic" off by default in v8.5 for	Hugo Herbelin	2015-05-09
*	Fix documentation of Redirect	Enrico Tassi	2015-05-04
*	More precise numbers about Benjamin's fix for the VM.	Maxime Dénès	2015-04-22
*	Update CHANGES	Matthieu Sozeau	2015-04-22
*	Removing references to -I -as from CHANGES.	Pierre-Marie Pédrot	2015-04-07
*	Accomodating #4166 (providing "Require Import OmegaTactic" as a	Hugo Herbelin	2015-04-01
*	Announcing * and ** which were not official yet in 8.4.	Hugo Herbelin	2015-03-22
*	Aliasing give_up with admit	Enrico Tassi	2015-03-22
*	CHANGES: more correct equivalent to "constructor tac" syntax.	Arnaud Spiwack	2015-03-13
*	admit: replaced by give_up + Admitted (no proof_admitted : False, close #4032)	Enrico Tassi	2015-03-11
*	Explicit in CHANGES incompatibilities introduced in patterns by b2953849 (or ...	Pierre Boutillier	2015-02-28
*	CHANGES: Info command + info_auto currently broken.	Arnaud Spiwack	2015-02-24
*	Undo: back to 8.4 semantics (Close #3514)	Enrico Tassi	2015-02-15
*	Note about "Undo. Undo." in CHANGES	Enrico Tassi	2015-02-15
*	Document the behavior change of Instance wrt {\|...\|}. (Fix for bug #3749)	Guillaume Melquiond	2015-02-15
*	Document the issue with trivial inductive types. (Workaround for bug #3984)	Guillaume Melquiond	2015-02-13
*	Fix typos about .vio files (thanks Arthur for spotting them)	Enrico Tassi	2015-02-12
*	Updating CHANGES (grammar, thanks to AS for pointing it out) +	Hugo Herbelin	2015-01-24
*	Typos, grammar, layout in CHANGES (continued).	Hugo Herbelin	2015-01-23
*	Typos, grammar, layout in CHANGES.	Hugo Herbelin	2015-01-23
*	Documenting the removal of coercions between sig, sigT, sig2,	Hugo Herbelin	2015-01-16
*	Move explanations about primitive projections to the manual.	Matthieu Sozeau	2015-01-15
*	Update header of CHANGES.	Maxime Dénès	2015-01-15
*	Mention guard condition in CHANGES.	Maxime Dénès	2015-01-15
*	CHANGES: my recent updates to Ltac.	Arnaud Spiwack	2015-01-14
*	More in CHANGES about local definitions	Pierre-Marie Pédrot	2015-01-13
*	CHANGES: mention "Optimize (Heap\|Proof)"	Enrico Tassi	2015-01-10
*	Update + English in CHANGES	Hugo Herbelin	2015-01-08
*	Start credits for 8.5.	Matthieu Sozeau	2015-01-08
*	Fixed and extend bullet related info/error messages. + doc.	Pierre Courtieu	2015-01-08
*	Document native_compute.	Maxime Dénès	2015-01-08
*	rename: vi -> vio	Enrico Tassi	2015-01-06
*	Document the new behavior of lazymatch.	Guillaume Melquiond	2014-12-30
*	more CHANGES	Enrico Tassi	2014-12-30
*	Minor modification of CHANGE.	Pierre Courtieu	2014-12-23
*	Better doc and a few fixes for Proof using.	Enrico Tassi	2014-12-19
*	In CHANGES, alerting about stronger check on notation level modifiers.	Hugo Herbelin	2014-12-16
*	About now accepts hypothesis names and goal selector.	Pierre Courtieu	2014-12-15
*	Searchxxx now search also the hypothesis and support goal selector.	Pierre Courtieu	2014-12-12