coq - The formal proof system

Age	Commit message (Expand)	Author
2015-01-29	Remove spurious "Loading ML file" and "<W> Grammar extension" from the refere...	Guillaume Melquiond
2015-01-29	Remove some "Warning:" from the reference manual.	Guillaume Melquiond
2015-01-29	Fix some typos in the documentation.	Guillaume Melquiond
2015-01-29	Fix some broken Coq scripts in the reference manual.	Guillaume Melquiond
2015-01-27	Doc: Overfull lines in chapter on Canonical Structures.	Hugo Herbelin
2015-01-24	Doc: Fixing some compilation problems with chapter Canonical	Hugo Herbelin
2015-01-24	Reference Manual: Documenting new printing of evars and new effect of	Hugo Herbelin
2015-01-21	Reference Manual/Credits: expand the paragraph on the new proof engine to mat...	Arnaud Spiwack
2015-01-21	Reference Manual/Credits: native compute is a major contribution.	Arnaud Spiwack
2015-01-21	Reference manual/Credits: populate the "various smaller-scale improvements" p...	Arnaud Spiwack
2015-01-21	Reference Manual/Credits: remove a duplicate.	Arnaud Spiwack
2015-01-21	Reference manual: pass over the credit section for English.	Arnaud Spiwack
2015-01-21	Reference manual: fix typo in doc of [tryif/then/else].	Arnaud Spiwack
2015-01-17	Univs: Complete documentation in refman.	Matthieu Sozeau
2015-01-15	Minor fixes to the refman credits to be continued.	Matthieu Sozeau
2015-01-15	Move explanations about primitive projections to the manual.	Matthieu Sozeau
2015-01-15	Expand Credits for 8.5 and doc on universes	Matthieu Sozeau
2015-01-15	Tentatively updating credits while remaining brief.	Hugo Herbelin
2015-01-14	Reference manual: I had previously omitted the syntax entry for [> t1\|…\|tn].	Arnaud Spiwack
2015-01-14	Reference manual: document tryif/then/else.	Arnaud Spiwack
2015-01-14	Reference manual: document multimatch.	Arnaud Spiwack
2015-01-14	Reference manual: try and improve documentation for Ltac's match.	Arnaud Spiwack
2015-01-14	Reference manual: try and improve the documentation of lazymatch.	Arnaud Spiwack
2015-01-14	Reference manual: document gfail.	Arnaud Spiwack
2015-01-13	More documentation of the Local Definitions and Axioms.	Pierre-Marie Pédrot
2015-01-11	some credits for STM	Enrico Tassi
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	Fix some documentation typos.	Guillaume Melquiond
2015-01-08	Document native_compute.	Maxime Dénès
2015-01-06	rename: vi -> vio	Enrico Tassi
2015-01-06	Fix some documentation typos.	Guillaume Melquiond
2015-01-05	Added more informative messages about bullets.	Pierre Courtieu
2015-01-05	Updating documentation about bullets.	Pierre Courtieu
2014-12-30	Document the new behavior of lazymatch.	Guillaume Melquiond
2014-12-25	Document 6d5b56d971 (forbid Require inside modules).	Maxime Dénès
2014-12-19	Better doc and a few fixes for Proof using.	Enrico Tassi
2014-12-18	Proof using: New vernacular to name sets of section variables	Enrico Tassi
2014-12-12	Searchxxx now search also the hypothesis and support goal selector.	Pierre Courtieu
2014-12-09	refman: switch all source files to utf8	Pierre Letouzey
2014-12-09	refman: fix broken urls	Pierre Letouzey
2014-12-09	refman/Omega.tex: do not advertize Pierre Cregut's email for bug reports	Pierre Letouzey
2014-12-09	refman/coqdoc.tex: fix two erroneous \url	Pierre Letouzey
2014-12-09	refman: for xhtml validity, add 'alt' attributes to img	Pierre Letouzey
2014-12-09	refman: avoid label names with whitespace (unsupported in html)	Pierre Letouzey
2014-11-30	Documenting the Set Refine Instance Mode.	Pierre-Marie Pédrot
2014-11-27	typos	Enrico Tassi
2014-11-17	Documenting the -color option.	Pierre-Marie Pédrot
2014-11-17	Documenting use of colors in Coq.	Pierre-Marie Pédrot
2014-11-16	Enforcing a stronger difference between the two syntaxes "simpl	Hugo Herbelin