coq - The formal proof system

Age	Commit message (Expand)	Author
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
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
2019-01-29	Use \mathcal instead of \cal	Gaëtan Gilbert
2019-01-28	Surround "assumption" with :tacn:`` in tactics.rst	Ryan Scott
2019-01-28	Merge PR #9402: Move \def\plus and \def\tri to refman-preamble.sty.	Théo Zimmermann
2019-01-28	Merge PR #9341: [ssr] uniform clear discipline	Maxime Dénès
2019-01-25	Merge PR #9391: Clarify meaning of Primitive Projections	Théo Zimmermann
2019-01-25	[Numeral notations] Lazy resolution of decimal types	Vincent Laporte
2019-01-24	Rename Z.div_mod_to_quot_rem, add Z.quot_rem_to_equations, Z.to_euclidean_div...	Jason Gross
2019-01-24	Revert "Add subst to the end of nia in the test-suite"	Jason Gross