aboutsummaryrefslogtreecommitdiff
path: root/doc/sphinx/language
AgeCommit message (Collapse)Author
2020-04-03Split four sections out of the Gallina extensions chapter.Théo Zimmermann
This octopus merge is meant to preserve the commit history / blame of all the parts.
2020-04-03Move section in records in appropriate location (inside core).Théo Zimmermann
2020-04-03Move section on sections in appropriate location (inside core).Théo Zimmermann
2020-04-03Move section on funind in appropriate location (inside libraries).Théo Zimmermann
2020-04-03Move section on implicit arguments in appropriate location (inside extensions).Théo Zimmermann
2020-04-03Extract section on implicit arguments from Gallina extensions.Théo Zimmermann
2020-04-03Extract section on funind from Gallina extensions.Théo Zimmermann
2020-04-03Remove sections on records, sections, funind and implicit arguments from ↵Théo Zimmermann
gallina-ext chapter.
2020-04-03Extract section on sections from Gallina extensions.Théo Zimmermann
2020-04-03Extract section on records from Gallina extensions.Théo Zimmermann
2020-03-29Merge PR #11859: Warn when non exactly parsing non floating-pointHugo Herbelin
Ack-by: SkySkimmer Reviewed-by: Zimmi48 Reviewed-by: erikmd
2020-03-26Merge PR #11877: Removing deprecated destruct/remember syntax _eqn.Théo Zimmermann
Reviewed-by: Zimmi48
2020-03-26Removing deprecated destruct syntax _eqn.Hugo Herbelin
2020-03-26Shrink refman-prelude files.Théo Zimmermann
2020-03-26Remove outdated mention of -allow-sprop.Théo Zimmermann
2020-03-26Print a warning when parsing non floating-point values.Pierre Roux
For instance, parsing 0.1 will print a warning whereas parsing 0.5 won't.
2020-03-25Doc_grammar: Update cmd:: and tacn:: constructs in .rstsJim Fehrle
Remove unneeded source and output files Move all commands under command NT Add a lot of edits for commands and tactics
2020-03-25Convert Gallina Extensions to use prodnJim Fehrle
2020-03-20Merge PR #11665: Make Cumulative, NonCumulative and Private attributes.Pierre-Marie Pédrot
Ack-by: SkySkimmer Reviewed-by: jfehrle Reviewed-by: ppedrot
2020-03-19Document all the existing attributes.Théo Zimmermann
And fix documentation following the removal of the Template Check flag in #11546.
2020-03-19Adapt to sub-TOC not showing in PDF output.Théo Zimmermann
2020-03-19[refman] Move chapters into new structure.Théo Zimmermann
As a first step toward a deeper refactoring of the reference manual, we move existing chapters into a new structure. We use the Sphinx support for top-level chapters spanning multiple pages to consolidate existing chapters into a smaller number of chapters and a smaller number of parts. Now the full top-level table of content can be seen in one glance. Most of the new chapters are divided into several sub-chapters (on separate pages) that correspond to the pre-existing chapters. These new top-level chapters gathering several chapters together have gained a new introduction. The main introduction has been rewritten / simplified as well. For now, the URL of pre-existing chapters does not change. The intent is to further refactor the manual by splitting some of these sub-chapters into smaller ones, and by moving things around. While the sub-chapters are likely to evolve very much in the future, the top-level table of content is almost final (except that the "Using Coq" part may gain one or two additional chapters on proof engineering / project management). Thanks to Jim Fehrle for investigating how to split a chapter on multiple pages and to both Jim and Matthieu Sozeau for the discussion that led to this new structure. See also the related CEP: https://github.com/coq/ceps/pull/43 Additional notes: - A new directory structure has been created reflecting the new chapter structure. - The indexes chapter has been removed from the PDF version since it wasn't working. Co-authored-by: Jim Fehrle <jfehrle@sbcglobal.net>
2020-03-09Remove some productionlistsJim Fehrle
2020-03-04Adding support for an "only parsing" modifier in "where"-based notations.Hugo Herbelin
Co-Authored-By: Théo Zimmermann <theo.zimmi@gmail.com>
2020-02-29Merge PR #11701: Fix #11696: link from refman to stdlib doc is dead.Clément Pit-Claudel
Reviewed-by: cpitclaudel
2020-02-28Convert Gallina Vernac to use prodnJim Fehrle
2020-02-27Fix #11696: link from refman to stdlib doc is dead.Théo Zimmermann
2020-02-21Merge PR #11261: Use implicit types for printing (granting wish #10366).Emilio Jesus Gallego Arias
Ack-by: SkySkimmer Ack-by: Zimmi48 Reviewed-by: ejgallego
2020-02-18Updating reference manual and adding a change log entry.Hugo Herbelin
Co-Authored-By: Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr>
2020-02-17New syntax [Inductive Acc A R | x : Prop := ...]Gaëtan Gilbert
to control uniform parameters. This replaces the attribute.
2020-02-17Revert "Add #[uniform] and #[nonuniform] (for Uniform Inductive Parameters)"Gaëtan Gilbert
This reverts commit bc2c1836ba4c878903288060bcb66a0ef1aaced6.
2020-02-14Merge PR #11584: Add #[uniform] and #[nonuniform] (for Uniform Inductive ↵Maxime Dénès
Parameters) Reviewed-by: Matafou Reviewed-by: Zimmi48 Reviewed-by: maximedenes
2020-02-13Add #[uniform] and #[nonuniform] (for Uniform Inductive Parameters)Gaëtan Gilbert
2020-02-13Arguments: removing the restriction to set an anonymous parameter implicit.Hugo Herbelin
This was already possible manually using "{ _ }" in the type of declaration. This was also possible for type classes. So, no reason to forbid in Arguments.
2020-02-11Document the ability to use manual implicit arguments in subexpressions.Hugo Herbelin
2020-02-04Apply suggestions from HugoSimonBoulier
Co-Authored-By: Hugo Herbelin <herbelin@users.noreply.github.com>
2020-02-04Update doc for non max implicit argumentsSimonBoulier
2020-01-19Merge PR #11368: Turn trailing implicit warning into an errorHugo Herbelin
Ack-by: Zimmi48 Reviewed-by: herbelin Ack-by: maximedenes
2020-01-09Merge PR #11164: [CS] allow Let variable to be canonicalPierre-Marie Pédrot
Ack-by: SkySkimmer Ack-by: Zimmi48 Ack-by: ejgallego Reviewed-by: ppedrot
2020-01-08Trailing implicit: Maxime's suggestionsSimonBoulier
2020-01-07Merge PR #11369: [refman] Correct manual about implicit parameters in inductivesThéo Zimmermann
Reviewed-by: Zimmi48
2020-01-07Correct manual about implicit parameters in inductives.SimonBoulier
2020-01-07Trailing implicit error: documentationSimonBoulier
2020-01-06doc: mention limitation of bidi hints vs programGaëtan Gilbert
No example as I'm not familiar enough with Program to make one.
2020-01-06Merge PR #11340: [refman] Fix bad quoting practice leftover from Sphinx ↵Clément Pit-Claudel
migration. Reviewed-by: jfehrle
2019-12-31Merge PR #11325: [refman] Add missing s.Pierre-Marie Pédrot
Reviewed-by: jfehrle
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-29Merge PR #11314: Convert productionlists in the Gallina chapter up to the ↵Théo Zimmermann
Vernacular section to prodns Reviewed-by: Zimmi48
2019-12-28Convert productionlists to prodnsJim Fehrle
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-23 09:28:03 +0000