coq - The formal proof system

Age	Commit message (Collapse)	Author
2018-06-21	Merge PR #7815: On cygwin, pass the filename in a format that coqdoc ↵	Maxime Dénès
	understands.
2018-06-20	On cygwin, pass the filename in a format that coqdoc understands.	Jim Fehrle

2018-06-19	[doc] Rewrite and document the prodn directive	Clément Pit-Claudel
	It was broken and undocumented. We dropped the git logs, too, so it wasn't clear who wrote it and why it was introduced in the first place.
2018-06-08	gitlab: build sphinx doc in separate job	Gaëtan Gilbert

2018-05-25	[doc] Allow more than one signature and name per Sphinx object	Clément Pit-Claudel
	As discussed in GH-7556.
2018-05-25	Merge PR #7556: Add a setting to warn about empty object in the refman	Maxime Dénès

2018-05-22	[doc] Add a setting to warn about empty Coq objects	Clément Pit-Claudel

2018-05-16	[sphinx] Bump timeout. Closes #7532.	Clément Pit-Claudel

2018-05-15	[doc] More feedback on doc writer guide	Clément Pit-Claudel
	Co-Authored-By: @Zimmi48
2018-05-15	[doc] Search for 'coqtop' in $PATH if COQBIN is unset	Clément Pit-Claudel

2018-05-15	[doc] Address feedback on doc writer guide	Clément Pit-Claudel
	Co-Authored-By: @Zimmi48
2018-05-15	[doc] Add a README to doc/sphinx/	Clément Pit-Claudel
	The readme is auto-generated by combining introductory text with the docstrings in coqdomain.py.
2018-05-15	[doc] Document all directives and roles of our Sphinx domain	Clément Pit-Claudel
	Also get rid of a few unused or redundant constructs: the :ltac: role and the 'tac' directive (unused) and the :gallina: and :notation: roles (redundant).
2018-05-15	[doc] Compute the path to coqdoc at run time, not at load time	Clément Pit-Claudel

2018-05-09	[sphinx] Warn for dangling tacn / cmd / opt / ... references.	Clément Pit-Claudel

2018-04-16	Merge PR #7251: doc: Rename UbuntuMono-Square to CoqNotations and tweak spacing	Maxime Dénès

2018-04-14	[Sphinx] Fix all remaining warnings.	Maxime Dénès

2018-04-14	doc: Rename UbuntuMono-Square to CoqNotations and tweak spacing	Clément Pit-Claudel
	The Ubuntu Font License requires substantially modified fonts to be renamed entirely.
2018-04-14	[Sphinx] Add chapter 9.	Théo Zimmermann
	Chapter ported by Théo Zimmermann and Maxime Dénès.
2018-04-09	[Sphinx] Make it possible to espace { by %{ in custom grammars	Maxime Dénès

2018-03-16	[Sphinx] Better error message for coqtop errors	Maxime Dénès

2018-03-16	[Sphinx] Increase coqtop timeout to avoid spurious failures on CI	Maxime Dénès

2018-03-12	[Sphinx] Add a few grammar constructions	Maxime Dénès
	Code from Paul Steckler (MIT).
2018-03-09	Moving Gitlab CI documentation build to the main Coq build.	Maxime Dénès

2018-03-09	Integration of a sphinx-based documentation generator.	Maxime Dénès
	The original contribution is from Clément Pit-Claudel. I updated his code and integrated it with the Coq build system. Many improvements by Paul Steckler (MIT). This commit adds the infrastructure but no content.