aboutsummaryrefslogtreecommitdiff
path: root/doc/sphinx/language
AgeCommit message (Collapse)Author
2018-07-19Rewrote section 'Accessing the Type level' in the chapter 'The Coq library' ↵Zeimer
of the Reference Manual.
2018-07-19Fixed some typos and grammar errors from section 'The language' of the ↵Zeimer
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.
2018-07-17Remove fourier pluginMaxime Dénès
As stated in the manual, the fourier tactic is subsumed by lra.
2018-07-12Tactic deprecation machineryMaxime Dénès
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.".
2018-07-09Merge PR #7920: Generic syntax for attributesMaxime Dénès
2018-07-04doc: Fix markup in Calculus of Inductive ConstructionsFabian
2018-07-03Describe attributes in the documentation.Vincent Laporte
2018-07-02Merge PR #7703: Add an option to force parameters to be uniformMatthieu Sozeau
2018-07-02Merge PR #7969: doc: typesetting and hyperlinks in Syntax ExtensionsThéo Zimmermann
2018-07-01Document option Uniform Inductive ParametersJasper Hugunin
2018-06-30doc: typesetting and hyperlinks in Syntax ExtensionsLysxia
2018-06-29doc: Fix typesetting in Gallina extensionsLysxia
2018-06-28wrong sphinx syntaxAmbroise
2018-06-28Update gallina-extensions.rstAmbroise
I knew this feature existed but I did not remember the syntax and I could not find it in the manual
2018-06-24Documenting the syntax of mutual keywords.Pierre-Marie Pédrot
2018-06-16[sphinx] Finish clean-up of the Canonical Structure subsection.Théo Zimmermann
2018-06-16doc: Add "Print Canonical Projections" command to Command indexAnton Trunov
2018-06-04Documenting the deprecation.Pierre-Marie Pédrot
2018-05-28Improve the last section of the Gallina chapter.Théo Zimmermann
2018-05-28Chapter 1 of the refman compiles without reporting any undocumented object.Théo Zimmermann
2018-05-28Improve sections on (Co)Fixpoint of the Gallina chapter.Théo Zimmermann
2018-05-27Improve subsection on co-inductive types of the Gallina chapter.Théo Zimmermann
2018-05-27Improve subsection on mutual inductive types of the Gallina chapter.Théo Zimmermann
2018-05-27Move 'new in Coq 8.1' subsection to an appropriate place.Théo Zimmermann
2018-05-27Document Variant properly.Théo Zimmermann
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).
2018-05-27Improve inductive types subsection of the Gallina chapter.Théo Zimmermann
2018-05-26Improve subsection Definitions of the Gallina chapter.Théo Zimmermann
2018-05-26Improve subsection Assumptions of the Gallina chapter.Théo Zimmermann
2018-05-26Improve the section Terms of the Gallina chapter.Théo Zimmermann
Including adding missing irrefutable-patterns to the grammar of binders.
2018-05-25[doc] Allow more than one signature and name per Sphinx objectClément Pit-Claudel
As discussed in GH-7556.
2018-05-21Document the new nested-proof error message.Théo Zimmermann
2018-05-17Document nested proofs and associated option.Théo Zimmermann
2018-05-15[doc] Address feedback on doc writer guideClément Pit-Claudel
Co-Authored-By: @Zimmi48
2018-05-14Remove duplicate entries for Proof, Qed, Defined, Admitted.Théo Zimmermann
And marginal improvements in the last section of the Gallina chapter.
2018-05-09[sphinx] Fix new warnings related to tacn, cmd, opt...Théo Zimmermann
2018-05-05[sphinx] Backport changes from #5979.Théo Zimmermann
2018-05-05Clean-up around cmd documentation.Théo Zimmermann
In particular, remove trailing dots.
2018-05-05Fix 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-05Clean-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[sphinx] Fix some references.Théo Zimmermann
2018-04-26Merge PR #7331: Fix a typo in the reference manual: <; -> <:Maxime Dénès
2018-04-26Merge PR #7181: Sphinx docs: clarify strict implicit arguments a bitMaxime Dénès
2018-04-23Fix a typo in the reference manual: <; -> <:Kazuhiko Sakaguchi
2018-04-16[Sphinx] Clean-up indicesMaxime Dénès
2018-04-16[Sphinx] Fix a lot of references and description of optionsMaxime Dénès
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-13[Sphinx] Add Chapter 1Maxime Dénès
2018-04-13[Sphinx] Move chapter 1 to new infrastructureMaxime Dénès
2018-04-12Merge PR #7222: [sphinx] Remove migration artefacts.Maxime Dénès
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-22 00:22:01 +0000