coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Rewrote section 'Accessing the Type level' in the chapter 'The Coq library' ↵	Zeimer	2018-07-19
\| \| \| \|	of the Reference Manual.
*	Fixed some typos and grammar errors from section 'The language' of the ↵	Zeimer	2018-07-19
\| \| \| \|	Reference Manual. Removed all mentions of prodT because it is no longer a separate inductive definition (prod has been living in Type for some time) but rather only a notation for prod needed for compatibility purposes.
*	Remove fourier plugin	Maxime Dénès	2018-07-17
\| \| \| \|	As stated in the manual, the fourier tactic is subsumed by lra.
*	Tactic deprecation machinery	Maxime Dénès	2018-07-12
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	We make it possible to deprecate tactics defined by `Ltac`, `Tactic Notation` or ML. For the first two variants, we anticipate the syntax of attributes: `#[deprecated(since = "XX", note = "YY")]` In ML, the syntax is: ``` let reflexivity_depr = let open CWarnings in { since = "8.5"; note = "Use admit instead." } TACTIC EXTEND reflexivity DEPRECATED reflexivity_depr [ "reflexivity" ] -> [ Tactics.intros_reflexivity ] END ``` A warning is shown at the point where the tactic is used (either a direct call or when defining another tactic): Tactic `foo` is deprecated since XX. YY YY is typically meant to be "Use bar instead.".
*	Merge PR #7920: Generic syntax for attributes	Maxime Dénès	2018-07-09
\|\
* \|	doc: Fix markup in Calculus of Inductive Constructions	Fabian	2018-07-04
\| \|
\| *	Describe attributes in the documentation.	Vincent Laporte	2018-07-03
\|/
*	Merge PR #7703: Add an option to force parameters to be uniform	Matthieu Sozeau	2018-07-02
\|\
* \	Merge PR #7969: doc: typesetting and hyperlinks in Syntax Extensions	Théo Zimmermann	2018-07-02
\|\ \
\| \| *	Document option Uniform Inductive Parameters	Jasper Hugunin	2018-07-01
\| \| \|
\| * \|	doc: typesetting and hyperlinks in Syntax Extensions	Lysxia	2018-06-30
\| \|/
* /	doc: Fix typesetting in Gallina extensions	Lysxia	2018-06-29
\|/
*	wrong sphinx syntax	Ambroise	2018-06-28
\|
*	Update gallina-extensions.rst	Ambroise	2018-06-28
\| \| \|	I knew this feature existed but I did not remember the syntax and I could not find it in the manual
*	Documenting the syntax of mutual keywords.	Pierre-Marie Pédrot	2018-06-24
\|
*	[sphinx] Finish clean-up of the Canonical Structure subsection.	Théo Zimmermann	2018-06-16
\|
*	doc: Add "Print Canonical Projections" command to Command index	Anton Trunov	2018-06-16
\|
*	Documenting the deprecation.	Pierre-Marie Pédrot	2018-06-04
\|
*	Improve the last section of the Gallina chapter.	Théo Zimmermann	2018-05-28
\|
*	Chapter 1 of the refman compiles without reporting any undocumented object.	Théo Zimmermann	2018-05-28
\|
*	Improve sections on (Co)Fixpoint of the Gallina chapter.	Théo Zimmermann	2018-05-28
\|
*	Improve subsection on co-inductive types of the Gallina chapter.	Théo Zimmermann	2018-05-27
\|
*	Improve subsection on mutual inductive types of the Gallina chapter.	Théo Zimmermann	2018-05-27
\|
*	Move 'new in Coq 8.1' subsection to an appropriate place.	Théo Zimmermann	2018-05-27
\|
*	Document Variant properly.	Théo Zimmermann	2018-05-27
\| \| \| \| \| \|	Cf. Enrico's remark at https://github.com/coq/coq/pull/7536#issuecomment-389826121 This commit also marginally improves the Record doc (a lot more remains to do).
*	Improve inductive types subsection of the Gallina chapter.	Théo Zimmermann	2018-05-27
\|
*	Improve subsection Definitions of the Gallina chapter.	Théo Zimmermann	2018-05-26
\|
*	Improve subsection Assumptions of the Gallina chapter.	Théo Zimmermann	2018-05-26
\|
*	Improve the section Terms of the Gallina chapter.	Théo Zimmermann	2018-05-26
\| \| \| \|	Including adding missing irrefutable-patterns to the grammar of binders.
*	[doc] Allow more than one signature and name per Sphinx object	Clément Pit-Claudel	2018-05-25
\| \| \| \|	As discussed in GH-7556.
*	Document the new nested-proof error message.	Théo Zimmermann	2018-05-21
\|
*	Document nested proofs and associated option.	Théo Zimmermann	2018-05-17
\|
*	[doc] Address feedback on doc writer guide	Clément Pit-Claudel	2018-05-15
\| \| \| \|	Co-Authored-By: @Zimmi48
*	Remove duplicate entries for Proof, Qed, Defined, Admitted.	Théo Zimmermann	2018-05-14
\| \| \| \|	And marginal improvements in the last section of the Gallina chapter.
*	[sphinx] Fix new warnings related to tacn, cmd, opt...	Théo Zimmermann	2018-05-09
\|
*	[sphinx] Backport changes from #5979.	Théo Zimmermann	2018-05-05
\|
*	Clean-up around cmd documentation.	Théo Zimmermann	2018-05-05
\| \| \| \|	In particular, remove trailing dots.
*	Fix error messages and make them consistent.	Théo Zimmermann	2018-05-05
\| \| \| \|	All the error messages start with a capitalized letter and end with a dot.
*	Clean-up around options.	Théo Zimmermann	2018-05-05
\| \| \| \| \| \|	- Remove all trailing dots. - There is only one Bullet Behavior option. - Replaces `@natural` and `@integer` by `@num`.
*	[sphinx] Fix some references.	Théo Zimmermann	2018-05-05
\|
*	Merge PR #7331: Fix a typo in the reference manual: <; -> <:	Maxime Dénès	2018-04-26
\|\
* \	Merge PR #7181: Sphinx docs: clarify strict implicit arguments a bit	Maxime Dénès	2018-04-26
\|\ \
\| \| *	Fix a typo in the reference manual: <; -> <:	Kazuhiko Sakaguchi	2018-04-23
\| \|/ \|/\|
* \|	[Sphinx] Clean-up indices	Maxime Dénès	2018-04-16
\| \|
* \|	[Sphinx] Fix a lot of references and description of options	Maxime Dénès	2018-04-16
\| \|
* \|	[Sphinx] Fix all remaining warnings.	Maxime Dénès	2018-04-14
\| \|
* \|	[sphinx] Fix many warnings.	Théo Zimmermann	2018-04-14
\| \| \| \| \| \| \| \| \| \|	Including cross-reference TODOs. I took down the number of warnings from 300 to 50.
* \|	[Sphinx] Add Chapter 1	Maxime Dénès	2018-04-13
\| \|
* \|	[Sphinx] Move chapter 1 to new infrastructure	Maxime Dénès	2018-04-13
\| \|
* \|	Merge PR #7222: [sphinx] Remove migration artefacts.	Maxime Dénès	2018-04-12
\|\ \