aboutsummaryrefslogtreecommitdiff
path: root/doc/sphinx/language/gallina-specification-language.rst
AgeCommit message (Expand)Author
2020-01-09Merge PR #11164: [CS] allow Let variable to be canonicalPierre-Marie Pédrot
2020-01-06Merge PR #11340: [refman] Fix bad quoting practice leftover from Sphinx migra...Clément Pit-Claudel
2019-12-31Merge PR #11325: [refman] Add missing s.Pierre-Marie Pédrot
2019-12-29Remove :flag: that appears in the outputJim Fehrle
2019-12-29[refman] Fix bad quoting practice leftover from Sphinx migration.Théo Zimmermann
2019-12-28Convert productionlists to prodnsJim Fehrle
2019-12-24[Attributes] accept #[canonical] (Let|Definition)Enrico Tassi
2019-12-22[refman] Add missing s.Théo Zimmermann
2019-11-20Update grammar in the Terms section of Gallina chapterJim Fehrle
2019-11-14Fix doc for universes(foo) attributesGaëtan Gilbert
2019-11-06Replace "option" in doc when it refers to a flagJim Fehrle
2019-10-30Implement the unsupported attribute error using the warning systemGaëtan Gilbert
2019-10-22documentation fixesAntonio Nikishaev
2019-08-16Add documentation for typing flags.SimonBoulier
2019-07-28Update documentation on tokens, use "int" and "num"Jim Fehrle
2019-06-06`deprecated` attribute support for notations and syntactic definitionsMaxime Dénès
2019-05-23do not parse `|` as infix in patterns; parse `|}` as `|` `}`Georges Gonthier
2019-05-19[refman] Misc fixes (indentation, whitespace, notation syntax)Clément Pit-Claudel
2019-04-02Allow underscores as comments in numeral constants.Pierre Roux
2019-04-02Update documentationPierre Roux
2019-03-18[Manual] Parametrize -> ParametErizeLysxia
2019-03-18[Manual] Move command Context after Let, and more polishingLysxia
2019-03-17[Manual] Move doc on Let into Section mechanism, and more polishingLysxia
2019-03-17[Manual] Gather section-specific commands in Section documentation (fix #9704)Lysxia
2019-03-17[Manual] Improve chapter Type classes, and add mention of Context under VariableLysxia
2019-03-14Documentation for SPropGaëtan Gilbert
2019-02-28[sphinx] Add warn option to coqtop directive.Théo Zimmermann
2019-02-12Fix failing coqtops in gallina-specification-language.rstGaëtan Gilbert
2019-01-22Remove unneeded | in productionlistsJim Fehrle
2018-12-19Fix typo in gallina specification language docyudetamago
2018-10-16Document the issue with positive coinductive types.Pierre-Marie Pédrot
2018-09-28Small fixes in attribute documentation.Théo Zimmermann
2018-09-26Allow successive attributes #[foo] #[bar]Gaëtan Gilbert
2018-09-20Rewrite "Flags, Options and Tables" section.Jim Fehrle
2018-09-17Add missing index entries.Théo Zimmermann
2018-08-31Uniformized many spelling variants. Added .. warning:: and .. seealso:: direc...Zeimer
2018-07-30[sphinx] Use arguments of '.. example::' directive as a titleClément Pit-Claudel
2018-07-12Tactic deprecation machineryMaxime Dénès
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-01Document option Uniform Inductive ParametersJasper Hugunin
2018-06-30doc: typesetting and hyperlinks in Syntax ExtensionsLysxia
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
2018-05-27Improve inductive types subsection of the Gallina chapter.Théo Zimmermann
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-26 05:03:32 +0000