coq - The formal proof system

Age	Commit message (Expand)	Author
2019-02-18	Merge PR #9568: Add test that we regenerated doc/sphinx/README.rst to linter	Théo Zimmermann
2019-02-18	Merge PR #9142: Disable Ltac backtraces	Hugo Herbelin
2019-02-18	Add diff rule for README.rst to dune refman-html alias	Gaëtan Gilbert
2019-02-14	Merge PR #9571: Document the now_show tactic.	Clément Pit-Claudel
2019-02-14	Document the now_show tactic.	Théo Zimmermann
2019-02-14	[Manual] Fix a reference	Vincent Laporte
2019-02-14	[Manual] Clean examples for `apply`	Vincent Laporte
2019-02-14	[Manual] Don’t use `Undo` in ssreflect examples	Vincent Laporte
2019-02-14	[Manual] Clean examples about `inversion` tactic	Vincent Laporte
2019-02-13	Merge PR #9450: Fix #9432: canonical structure and coercion accept universe b...	Maxime Dénès
2019-02-13	[ssr] move shorter Canonical to Coq proper	Enrico Tassi
2019-02-13	Merge PR #9564: Fix small errors in cic.rst (3rd)	Théo Zimmermann
2019-02-13	Merge PR #9553: Sphinx various fixing of failing commands	Théo Zimmermann
2019-02-12	Fix failing coqtops in syntax-extensions.rst	Gaëtan Gilbert
2019-02-12	Fix failing coqtops in tactics.rst	Gaëtan Gilbert
2019-02-12	Fix failing coqtops in ssreflect-proof-language.rst	Gaëtan Gilbert
2019-02-12	Fix failing coqtops in ltac.rst	Gaëtan Gilbert
2019-02-12	Fix failing coqtops in coqide.rst	Gaëtan Gilbert
2019-02-12	Fix failing coqtops in gallina-specification-language.rst	Gaëtan Gilbert
2019-02-12	Fix failing coqtops in gallina-extensions.rst	Gaëtan Gilbert
2019-02-12	Fix failing coqtops in coq-library.rst	Gaëtan Gilbert
2019-02-12	Fix failing coqtops in cic.rst	Gaëtan Gilbert
2019-02-12	Fix failing coqtops universe-polymorphism.rst	Gaëtan Gilbert
2019-02-12	Improve the documentation of auto.	Théo Zimmermann
2019-02-12	Fix failing coqtops in ring.rst	Gaëtan Gilbert
2019-02-12	Fix failing coqtops in micromega.rst (the main one requires csdp)	Gaëtan Gilbert
2019-02-12	Fix failing coqtops in generalized-rewriting.rst	Gaëtan Gilbert
2019-02-12	Fix failing coqtops in extended-pattern-matching.rst	Gaëtan Gilbert
2019-02-12	Increase sphinx recursion limit	Gaëtan Gilbert
2019-02-11	Small typos in the documentation.	Martin Bodin
2019-02-11	Use math mode more.	Tanaka Akira
2019-02-11	Use {LEFT,RIGHT} DOUBLE QUOTATION MARK.	Tanaka Akira
2019-02-11	Remove a space before closing double-quote.	Tanaka Akira
2019-02-10	Change "I" to "I_p".	Tanaka Akira
2019-02-10	Distinguish inductive {definition,inductive}.	Tanaka Akira
2019-02-08	Use math mode more.	Tanaka Akira
2019-02-08	Fix index of arguments of constructor in fixpoint.	Tanaka Akira
2019-02-08	Change parameters p_1...p_r to q_1...q_r.	Tanaka Akira
2019-02-08	Change the index "p" to "s" in "type of branches".	Tanaka Akira
2019-02-08	Change c to c' forgotten at exchanging c and c'.	Tanaka Akira
2019-02-08	Remove spaces just before period (non-math mode).	Tanaka Akira
2019-02-08	Remove spaces just before comma (non-math mode).	Tanaka Akira
2019-02-08	Remove "'" accidentaly added.	Tanaka Akira
2019-02-06	Merge PR #9124: Document the possibility of declaring a Ltac name_goal.	Clément Pit-Claudel
2019-02-06	Merge PR #9456: The lowest universe level is 1.	Théo Zimmermann
2019-02-06	Document the possibility of declaring a Ltac name_goal.	Théo Zimmermann
2019-02-05	Documenting the Ltac Backtrace flag.	Pierre-Marie Pédrot
2019-02-05	Add advice and an example to the documentation of fold.	Théo Zimmermann
2019-02-04	Primitive integers	Maxime Dénès
2019-02-01	Merge PR #8062: Add Z.div_mod_to_quot_rem tactic, put it in zify	Vincent Laporte