coq - The formal proof system

Age	Commit message (Expand)	Author
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-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	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
2019-02-01	Merge PR #9095: [toplevel] Deprecate `-compile` flag in favor of `coqc`	Maxime Dénès
2019-02-01	The lowest universe level is 1.	Tanaka Akira
2019-01-31	Use λ instead of \lb.	Tanaka Akira
2019-01-31	The subst Γ{c}{(c c')} should be Γ{c'}{(c' c)}.	Tanaka Akira
2019-01-31	Use "U" instead of "u" for a type.	Tanaka Akira
2019-01-31	Fix an index. The number of constructors is "l".	Tanaka Akira
2019-01-31	Use \Match for match construct.	Tanaka Akira
2019-01-31	Insert a space before \kwend.	Tanaka Akira
2019-01-31	Use \length for the function name of length.	Tanaka Akira
2019-01-31	Adjust spaces.	Tanaka Akira
2019-01-31	Use "∀" and "λ" instead of \forall and \lambda.	Tanaka Akira
2019-01-31	Use math more.	Tanaka Akira
2019-01-31	Make parenthesis correctly matched.	Tanaka Akira
2019-01-31	\Sort is not a term.	Tanaka Akira
2019-01-31	Use semicolon for separator of local contexts.	Tanaka Akira
2019-01-31	Don't line break at hyphen of compound words.	Tanaka Akira
2019-01-31	Move out a period and comma from :math:.	Tanaka Akira
2019-01-31	Nest :math: and parenthesis properly.	Tanaka Akira
2019-01-31	Fix syntax of two lambda-abstractions.	Tanaka Akira
2019-01-31	Change {\Sort} to \Sort.	Tanaka Akira
2019-01-31	Use \Prop, \Set and \Type defined in refman-preamble.sty.	Tanaka Akira
2019-01-31	Make "1" and "2" in "f1" and "f2" suffixes.	Tanaka Akira
2019-01-31	Make "1" and "n" in "u1" and "un" suffixes.	Tanaka Akira
2019-01-31	Remove "End TreeExample." line.	Tanaka Akira
2019-01-31	Merge PR #8720: [Numeral notations] Use Coqlib registered constants	Emilio Jesus Gallego Arias
2019-01-30	[toplevel] Deprecate the `-compile` flag in favor of `coqc`.	Emilio Jesus Gallego Arias