coq - The formal proof system

Age	Commit message (Collapse)	Author
2018-05-05	[sphinx] Use references for command Info.	Théo Zimmermann

2018-05-05	[sphinx] More reference fixes.	Théo Zimmermann

2018-05-05	[sphinx] Use references for Print.	Théo Zimmermann

2018-05-05	Fix error messages and make them consistent.	Théo Zimmermann
	All the error messages start with a capitalized letter and end with a dot.
2018-05-05	Add direct reference to congruence with.	Théo Zimmermann

2018-05-05	Clean-up around options.	Théo Zimmermann
	- Remove all trailing dots. - There is only one Bullet Behavior option. - Replaces `@natural` and `@integer` by `@num`.
2018-05-05	debug trivial and debug auto were not in the tactic index.	Théo Zimmermann

2018-05-05	[sphinx] Fix some references.	Théo Zimmermann

2018-05-05	[sphinx] Backport reformulation.	Théo Zimmermann
	(cf. 711b9d8cdf6e25690d247d9e8c49f005527e64e2)
2018-05-05	[sphinx] Backport fix of typo.	Théo Zimmermann
	(cf. 6131f89f6b91c45e641dd877df8719fa77987453)
2018-05-02	Make "intro"/"intros" progress on existential variables.	Hugo Herbelin

2018-04-29	Strict focusing using Default Goal Selector.	Gaëtan Gilbert
	We add a [SelectAlreadyFocused] constructor to [goal_selector] (read "!") which causes a failure when there's not exactly 1 goal and otherwise is a noop. Then [Set Default Goal Selector "!".] puts us in "strict focusing" mode where we can only run tactics if we have only one goal or use a selector. Closes #6689.
2018-04-16	Merge PR #7270: Sphinx doc fix indices	Maxime Dénès

2018-04-16	[Sphinx] Clean-up indices	Maxime Dénès

2018-04-16	Merge PR #7264: [Sphinx] Fix a lot of references and description of options	Maxime Dénès

2018-04-16	[Sphinx] Fix a lot of references and description of options	Maxime Dénès

2018-04-16	Document the Export Set/Unset commands.	Pierre-Marie Pédrot
	Fixes #6963.
2018-04-14	[Sphinx] Fix all remaining warnings.	Maxime Dénès

2018-04-14	[sphinx] Fix many warnings.	Théo Zimmermann
	Including cross-reference TODOs. I took down the number of warnings from 300 to 50.
2018-04-14	[Sphinx] Add chapter 9.	Théo Zimmermann
	Chapter ported by Théo Zimmermann and Maxime Dénès.
2018-04-14	[Sphinx] Move chapter 9 to new infrastructure.	Théo Zimmermann

2018-04-13	Merge PR #7117: Sphinx doc chapter 29	Théo Zimmermann

2018-04-12	[Sphinx] Add chapter 29	Maxime Dénès
	Thanks to Clément Pit Claudel for porting this chapter. Backport universe polymorphism changes from 2017 and 2018.
2018-04-11	[sphinx] Remove migration artefacts.	Théo Zimmermann
	These were used very inconsistenty, serve no purpose and the link to the source is particularly useless because it's a moving target.
2018-04-11	Merge PR #6955: Fixed many typos and grammar errors in chapter 11 of the manual.	Maxime Dénès

2018-04-10	[Sphinx] Add chapter 6	Maxime Dénès
	Thanks to Yves Bertot for porting this chapter.
2018-04-10	[Sphinx] Move chapter 6 to new infrastructure	Maxime Dénès

2018-04-09	Merge PR #7162: Sphinx doc chapter 7	Théo Zimmermann

2018-04-09	[Sphinx] Add chapter 7	Maxime Dénès
	Thanks to Laurent Théry for porting this chapter.
2018-04-09	[Sphinx] Move chapter 7 to new infrastructure	Maxime Dénès

2018-04-06	Fixed many typos and grammar errors in chapter 11 of the manual.	Zeimer

2018-03-25	Clarify wording in tactics documentation.	Théo Zimmermann
	Closes #6980.
2018-03-16	[Sphinx] Add chapter 11	Maxime Dénès
	Thanks to Enrico Tassi, Assia Mahboubi, Laurence Rideau and Yves Bertot for porting this chapter.
2018-03-15	[Sphinx] Add chapter 10	Maxime Dénès
	Thanks to Calvin Beck for porting this chapter.
2018-03-15	[Sphinx] Move chapter 10 to new infrastructure	Maxime Dénès

2018-03-15	[Sphinx] Add chapter 8	Maxime Dénès
	Thanks to Heiko Becker and Nikita Zyuzin for porting this chapter.
2018-03-15	[Sphinx] Move chapter 8 to new infrastructure	Maxime Dénès