coq - The formal proof system

Age	Commit message (Expand)	Author
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	Fix doc for coqtop:: undo	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	Fix #9527: unknown evar in nonterminating [fix] error.	Gaëtan Gilbert
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-09	Update link to refman and stdlib doc for master branch.	Théo Zimmermann
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
2019-02-01	Merge PR #9095: [toplevel] Deprecate `-compile` flag in favor of `coqc`	Maxime Dénès
2019-02-01	Correct W-Ind.	Tanaka Akira
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