aboutsummaryrefslogtreecommitdiff
path: root/doc/sphinx/language
AgeCommit message (Collapse)Author
2018-09-20Rewrite "Flags, Options and Tables" section.Jim Fehrle
Mark boolean-valued options with :flag: Adjust tactic and command names so parameters aren't shown in the index unless they're needed for disambiguation. Remove references to synchronous options. Revise doc for tables. Correct indentation for text below :flag:
2018-09-20[doc] Fix more duplicate-label issues in production listsClément Pit-Claudel
2018-09-20[doc] Include the rst and LaTeX preambles automatically in all filesClément Pit-Claudel
2018-09-20[doc] Fix a few LaTeX mistakesClément Pit-Claudel
2018-09-19Merge PR #7343: Add missing index entries.Maxime Dénès
2018-09-17Add missing index entries.Théo Zimmermann
In particular, this backports e26b67436d12da63a11f0727c5b5895dfd03d249.
2018-09-16Mising prime in the subtyping rulesJoachim Breitner
2018-09-16Missing space in cic.rstJoachim Breitner
2018-09-13Add doc for template polymorphism option and attributes.Gaëtan Gilbert
2018-08-31Uniformized many spelling variants. Added .. warning:: and .. seealso:: ↵Zeimer
directives in many places. Disambiguated terminology: disequality now means <> while inequality means < <= > >=. Fixed some more grammar and spelling issues.
2018-08-27Fix a casing problem noticed by Lars Dölle on Coq-Club.Théo Zimmermann
2018-08-16Merge PR #8111: Docs: Fix p values in CIC Inductive Defs examplesMaxime Dénès
2018-07-30[sphinx] Use arguments of '.. example::' directive as a titleClément Pit-Claudel
Most existing uses of .. example did not use the first line as a title, so this commit also adds appropriate blank lines.
2018-07-23Add test for repeated section with same nameJasper Hugunin
2018-07-22Docs: minor typo in "Template Polymorphism"Timothy Bourke
2018-07-22Docs: minor typo in W-Ind relative to textTimothy Bourke
The rule uses s'_j, the text refers to s_j, the latter is simpler in the absence of any other constraints.
2018-07-21Docs: Fix p values in CIC Inductive Defs examplesTimothy Bourke
It seems that p is a natural number, so why not write it as 0 rather than the empty list for tree and forest? And, if I understand correctly, odd and even have p = 0 and Arr(even) = Arr(odd) = 1.
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-02 11:09:20 +0000