aboutsummaryrefslogtreecommitdiff
path: root/doc/sphinx/language
AgeCommit message (Expand)Author
2020-04-03Extract section on funind from Gallina extensions.Théo Zimmermann
2020-04-03Remove sections on records, sections, funind and implicit arguments from gall...Théo Zimmermann
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
2020-03-26Merge PR #11877: Removing deprecated destruct/remember syntax _eqn.Théo Zimmermann
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
2020-03-25Doc_grammar: Update cmd:: and tacn:: constructs in .rstsJim Fehrle
2020-03-25Convert Gallina Extensions to use prodnJim Fehrle
2020-03-20Merge PR #11665: Make Cumulative, NonCumulative and Private attributes.Pierre-Marie Pédrot
2020-03-19Document all the existing attributes.Théo Zimmermann
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
2020-03-09Remove some productionlistsJim Fehrle
2020-03-04Adding support for an "only parsing" modifier in "where"-based notations.Hugo Herbelin
2020-02-29Merge PR #11701: Fix #11696: link from refman to stdlib doc is dead.Clément Pit-Claudel
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
2020-02-18Updating reference manual and adding a change log entry.Hugo Herbelin
2020-02-17New syntax [Inductive Acc A R | x : Prop := ...]Gaëtan Gilbert
2020-02-17Revert "Add #[uniform] and #[nonuniform] (for Uniform Inductive Parameters)"Gaëtan Gilbert
2020-02-14Merge PR #11584: Add #[uniform] and #[nonuniform] (for Uniform Inductive Para...Maxime Dénès
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
2020-02-11Document the ability to use manual implicit arguments in subexpressions.Hugo Herbelin
2020-02-04Apply suggestions from HugoSimonBoulier
2020-02-04Update doc for non max implicit argumentsSimonBoulier
2020-01-19Merge PR #11368: Turn trailing implicit warning into an errorHugo Herbelin
2020-01-09Merge PR #11164: [CS] allow Let variable to be canonicalPierre-Marie Pédrot
2020-01-08Trailing implicit: Maxime's suggestionsSimonBoulier
2020-01-07Merge PR #11369: [refman] Correct manual about implicit parameters in inductivesThéo Zimmermann
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
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-29Merge PR #11314: Convert productionlists in the Gallina chapter up to the Ver...Théo Zimmermann
2019-12-28Convert productionlists to prodnsJim Fehrle
2019-12-28Update doc/sphinx/language/gallina-extensions.rstKazuhiko Sakaguchi
2019-12-28Extend `Print Canonical Projections` with a search functionalityKazuhiko Sakaguchi
2019-12-24[Attributes] accept #[canonical] (Let|Definition)Enrico Tassi
2019-12-22[refman] Add missing s.Théo Zimmermann
2019-12-02[CS] support #[local] attributeEnrico Tassi
2019-11-20Update grammar in the Terms section of Gallina chapterJim Fehrle
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-21 22:08:39 +0000