coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	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
*	Documenting the new Undo semantics	Enrico Tassi	2014-09-09
*	Removing the documentation of the XML plugin.	Pierre-Marie Pédrot	2014-09-08
*	CHANGES: existential variables are always "substituted" in the new tactic eng...	Arnaud Spiwack	2014-09-08
*	CHANGES: Ltac's [refine] accepts [uconstr].	Arnaud Spiwack	2014-09-08
*	CHANGES: [revgoals].	Arnaud Spiwack	2014-09-08
*	CHANGES: [Variant], [Set Nonrecursive Elimination Schemes].	Arnaud Spiwack	2014-09-08
*	CHANGES: binder names from Ltac identifiers.	Arnaud Spiwack	2014-09-08
*	"allows to", like "allowing to", is improper	Jason Gross	2014-08-25
*	Grammar: "allowing to" is not proper English	Jason Gross	2014-08-25
*	Adding a new intro-pattern for "apply in" on the fly. Using syntax	Hugo Herbelin	2014-08-18
*	Uncountably many bullets (+,-,,++,--,*,+++,...).	Hugo Herbelin	2014-08-05