coq - The formal proof system

Age	Commit message (Expand)	Author
2015-11-26	Adding the Printing Projections options to the index.	Pierre-Marie Pédrot
2015-11-07	Fixing documention of Add Printing Coercion.	Hugo Herbelin
2015-11-04	Univs: update refman, better printers for universe contexts.	Matthieu Sozeau
2015-11-04	Hint Cut documentation and cleanup of printing (was duplicated and	Matthieu Sozeau
2015-10-18	Reference Manual: Applying standard style recommendation about not	Hugo Herbelin
2015-10-14	Fix some typos.	Guillaume Melquiond
2015-10-13	Fix some typos.	Guillaume Melquiond
2015-10-11	Documenting matching under binders.	Hugo Herbelin
2015-10-10	Fix a few latex errors in documentation of Proof Using (e.g. \tt*).	Guillaume Melquiond
2015-10-08	Proof using: let-in policy, optional auto-clear, forward closure*	Enrico Tassi
2015-10-04	Fix typo. (Fix bug #4355)	Guillaume Melquiond
2015-10-02	Mark the Coq.Compat files for documentation. (Fix bug #4353)	Guillaume Melquiond
2015-10-02	Fixing error messages about Hint.	Hugo Herbelin
2015-10-02	Improving reference manual in that auto uses simple apply rather than apply.	Hugo Herbelin
2015-09-30	Fixing documentation wrt the ctrl-shift-u Unicode input method (see #2013).	Hugo Herbelin
2015-09-28	Make -load-vernac-object respect the loadpath.	Guillaume Melquiond
2015-09-26	Documenting how to support some special unicode characters in coqdoc	Hugo Herbelin
2015-09-26	Clarifying the doc of coqdoc --utf8 as discussed on coq-club on August 19, 2015.	Hugo Herbelin
2015-09-25	The -require option now accepts a logical path instead of a physical one.	Pierre-Marie Pédrot
2015-09-25	Updating the documentation and the toolchain w.r.t. the change in -compile.	Pierre-Marie Pédrot
2015-09-21	Fixing tutorial.	Pierre-Marie Pédrot
2015-09-10	typo in refman.	Pierre Courtieu
2015-08-17	Remove generatable documentation files from repository. (Fix bug #4315)	Guillaume Melquiond
2015-08-02	Granting Jason's request for an ad hoc compatibility option on	Hugo Herbelin
2015-07-31	Fix typos in the Extraction part of the reference manual.	Guillaume Melquiond
2015-07-31	Fix typos in the Micromega part of the reference manual.	Guillaume Melquiond
2015-07-31	Improve the table of content of the reference manual.	Guillaume Melquiond
2015-07-31	Remove some outdated files and fix permissions.	Guillaume Melquiond
2015-07-30	Avoid suggesting elim and decompose in the FAQ.	Guillaume Melquiond
2015-07-30	Remove some output of Qed in the FAQ.	Guillaume Melquiond
2015-07-30	Fix some broken Coq scripts in the documentation.	Guillaume Melquiond
2015-07-29	Improve the FAQ a bit.	Guillaume Melquiond
2015-07-28	Reset a dangling proof in the FAQ.	Guillaume Melquiond
2015-07-26	Regenerate the axiom figure of the FAQ.	Guillaume Melquiond
2015-07-26	Remove obsolete question about eta-conversion.	Guillaume Melquiond
2015-07-22	Refman: document Show Universes.	Matthieu Sozeau
2015-07-22	Remove obsolete documentation. (Fix bug #4238)	Guillaume Melquiond
2015-07-08	Fix documentation of universes.	Matthieu Sozeau
2015-07-08	Fix documentation.	Guillaume Melquiond
2015-07-07	Document Set/Print Firstorder Solver option.	Matthieu Sozeau
2015-06-26	Introduction of a "Undelimit Scope" command, undoing "Delimit Scope"	Lionel Rieg
2015-06-26	Typos in my previous edition of the reference manual.	Assia Mahboubi
2015-06-26	Some edition in the coq_makefile/_CoqProject section.	Assia Mahboubi
2015-06-26	Added _CoqProject to the index of the reference manual.	Assia Mahboubi
2015-06-17	Doc: Workers do check for guardedness before sending proofs back	Enrico Tassi
2015-05-13	Documenting Set Regular Subst Tactic (though unsure this is worth the	Hugo Herbelin
2015-05-13	Documenting the Loose Hint Behavior flag.	Pierre-Marie Pédrot
2015-05-04	Fix documentation of Redirect	Enrico Tassi
2015-05-04	Add a [Redirect] vernacular command	Clément Pit--Claudel
2015-04-17	Fixing a few typos + some uniformization of writing in doc.	Hugo Herbelin