coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	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
*	Documenting the Set Refine Instance Mode.	Pierre-Marie Pédrot	2014-11-30
*	Hopefully the last word on having "simpl f" complying with the	Hugo Herbelin	2014-11-18
*	Fixing detection of occurrences in the presence of nested subterms for	Hugo Herbelin	2014-11-18
*	Documenting use of colors in Coq.	Pierre-Marie Pédrot	2014-11-17
*	Enforcing a stronger difference between the two syntaxes "simpl	Hugo Herbelin	2014-11-16
*	Updating CHANGES (evars as ident).	Hugo Herbelin	2014-11-11
*	American spelling + layout in CHANGES.	Hugo Herbelin	2014-11-11
*	Fixing careless name confusion in CHANGES.	Pierre-Marie Pédrot	2014-11-04
*	Documenting the change of semantics of the replace tactic.	Pierre-Marie Pédrot	2014-11-04
*	Improving elimination with indices, getting rid of intrusive residual	Hugo Herbelin	2014-11-02
*	This commit introduces changes in induction and destruct.	Hugo Herbelin	2014-10-25
*	Documenting some incompatibilities in (non) Import of ML tactics,	Hugo Herbelin	2014-10-24
*	Addressing report #3279 (inconsistency of behavior of the -> and <-	Hugo Herbelin	2014-10-24
*	CHANGES: makes explicit the incompatibily introduced by the use of Ltac-defin...	Arnaud Spiwack	2014-10-22
*	Mentioning incompatibility shown in #3718 and coming from #3050	Hugo Herbelin	2014-10-13
*	Documenting option -type-in-type.	Hugo Herbelin	2014-09-29
*	Fixing inversion after having fixed intros_replacing	Hugo Herbelin	2014-09-10