coq - The formal proof system

Age	Commit message (Expand)	Author
2016-12-26	Fix broken documentation in presence of \zeroone{... \tt ...}.	Guillaume Melquiond
2016-12-26	Update documentation (bugs #5246 and #5251).	Guillaume Melquiond
2016-12-26	Fix some documentation typos.	Guillaume Melquiond
2016-10-19	Documenting Hint Resolve -> and <- variants.	Théo Zimmermann
2016-10-19	Making the doc of auto hints more precise.	Théo Zimmermann
2016-10-18	Extending the doc with a general summary of auto variants.	Théo Zimmermann
2016-10-18	Document info_auto.	Théo Zimmermann
2016-10-18	Improve the documentation of eauto.	Théo Zimmermann
2016-09-27	Fixing #4887 (confusion between using and with in documentation of firstorder).	Hugo Herbelin
2016-09-19	Replace { command ; } with ( command )	Erik Martin-Dorel
2016-09-19	Fix typos in RefMan-uti.tex.	Erik Martin-Dorel
2016-08-04	Fix documentation typo (bug #4994).	Guillaume Melquiond
2016-06-20	Reference Manual / Extraction: the original example command no longer works w...	Matej Kosik
2016-05-03	In Regular Subst Tactic mode, ensure that the order of hypotheses is	Hugo Herbelin
2016-04-28	Update tutorial (fix bug #4699).	Guillaume Melquiond
2016-04-12	FIX: HTML version of Chapter 4 of the Reference Manual	Matej Kosik
2016-04-12	TYPOGRAPHY: adding missing \noindent macros	Matej Kosik
2016-02-24	Document Hint Mode, cleanup Hint doc.	Matthieu Sozeau
2016-01-20	Update copyright headers.	Maxime Dénès
2016-01-20	Change $(...)$ to ltac:(...) in section 2.11. Fixes #4500.	Maxime Dénès
2016-01-20	Documenting Set Bullet Behavior.	Hugo Herbelin
2016-01-20	Clarifying the documentation of tactics "cbv" and "lazy".	Hugo Herbelin
2016-01-15	Thanks Hugo, but let's remain factual.	Maxime Dénès
2016-01-13	MMaps: remove it from final 8.5 release, since this new library isn't mature ...	Pierre Letouzey
2016-01-12	Referring to coq.inria.fr/stdlib for more on libraries and ltac-level tactics.	Hugo Herbelin
2016-01-12	Documenting dtauto and dintuition.	Hugo Herbelin
2016-01-12	Documenting options "Intuition Negation Unfolding", "Intuition Iff Unfolding".	Hugo Herbelin
2016-01-12	Documenting option 'Set Bracketing Last Introduction Pattern'.	Hugo Herbelin
2016-01-12	restore documentation of admit	Enrico Tassi
2016-01-06	Fix description of command-line options in the manual.	Guillaume Melquiond
2015-12-16	Updating credits.	Hugo Herbelin
2015-12-16	Add a "simple refine" variant of "refine" that does not call "shelve_unifiable".	Guillaume Melquiond
2015-12-15	Proof using: do not clear unused section hyps automatically	Enrico Tassi
2015-12-14	Fix \label which was meants to be \ref in doc of CIC terms.	Maxime Dénès
2015-12-14	Remove a mention of Set Virtual Machine in doc.	Maxime Dénès
2015-12-14	Moved proof_admitted to its own file, named "AdmitAxiom.v".	Maxime Dénès
2015-12-12	Extraction: documentation of the new option Unset Extraction SafeImplicits	Pierre Letouzey
2015-12-12	Indexing and documenting some options.	Pierre-Marie Pédrot
2015-12-11	Remove Set Virtual Machine from doc, since the command itself has been removed.	Maxime Dénès
2015-12-10	Changing syntax of pat/constr1.../constrn into pat%constr1...%constrn.	Hugo Herbelin
2015-12-10	Refman, ch. 4: A few fixes.	Hugo Herbelin
2015-12-10	ENH: redundant examples were removed	Matej Kosik
2015-12-10	FIX: wrong reference to a figure	Matej Kosik
2015-12-10	CLEANUP: putting examples inside "figure" environment	Matej Kosik
2015-12-10	ENH: The definition of the "_ ; _" operation on local context was added.	Matej Kosik
2015-12-10	TYPOGRAPHY: adjustments	Matej Kosik
2015-12-10	PROPOSITION: the side-condition was made more specific.	Matej Kosik
2015-12-10	PROPOSITION: rephrasing of the explanation of the meaning of '[I:A\|B]'	Matej Kosik
2015-12-10	PROPOSITION: Added an explicit definition of the notation for enriching the g...	Matej Kosik
2015-12-10	PROPOSITION: Added "if" and "then" words missing in the original sentence.	Matej Kosik