coq - The formal proof system

Age	Commit message (Expand)	Author
2019-02-01	[toplevel] Split interactive toplevel and compiler binaries.	Emilio Jesus Gallego Arias
2019-02-01	Merge PR #9415: Simplify the GitHub issue template	Maxime Dénès
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	Fix off-by-one error in nat syntax warnings	Jason Gross
2019-01-31	add test	Enrico Tassi
2019-01-31	[proof] optimize proof always works on incomplete proofs	Enrico Tassi
2019-01-31	Merge PR #9449: Fix small errors in cic.rst (2nd).	Théo Zimmermann
2019-01-31	Merge PR #9448: [ci] [ocaml] Fix OCaml trunk builds.	Gaëtan Gilbert
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	[ci] [ocaml] Fix OCaml trunk builds.	Emilio Jesus Gallego Arias
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	Merge PR #9442: Update pinned nixpkgs.	Vincent Laporte
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	Update Cachix signing key.	Théo Zimmermann
2019-01-30	Updated pinned nixpkgs.	Théo Zimmermann
2019-01-30	Merge PR #9440: Create deployment environment for Cachix.	Emilio Jesus Gallego Arias
2019-01-30	Create deployment environment for Cachix.	Théo Zimmermann
2019-01-30	[toplevel] Deprecate the `-compile` flag in favor of `coqc`.	Emilio Jesus Gallego Arias
2019-01-30	Cleanup universe length for inductives in vconv	Gaëtan Gilbert
2019-01-30	Restrict universes in records.	Gaëtan Gilbert
2019-01-30	Comment universe operations in Classes.context	Gaëtan Gilbert
2019-01-30	Merge pull request coq/ltac2#100 from JasonGross/fix-lazy-match-goal	Pierre-Marie Pédrot
2019-01-29	Merge PR #9417: Update update-compat.py script	Théo Zimmermann
2019-01-29	Merge PR #9435: Use \mathcal instead of \cal	Théo Zimmermann
2019-01-29	Update update-compat.py script	Jason Gross
2019-01-29	Merge PR #9274: Make `Instance` without a body always open a proof	Enrico Tassi
2019-01-29	[test-suite] Display full paths on CHECK.	Emilio Jesus Gallego Arias
2019-01-29	Use \mathcal instead of \cal	Gaëtan Gilbert