aboutsummaryrefslogtreecommitdiff
path: root/doc/sphinx/proof-engine/vernacular-commands.rst
AgeCommit message (Expand)Author
2020-11-14Distinguish one_pattern and one_term nonterminalsJim Fehrle
2020-11-12Clarifying the role of Add ML Path vs -I (see #13344).Hugo Herbelin
2020-11-09[refman] Stop applying a special style to Coq, CoqIDE, OCaml and Gallina.Théo Zimmermann
2020-11-05Various fixes.Théo Zimmermann
2020-10-24Convert misc chapters to prodnJim Fehrle
2020-10-20Add some missing smallcaps.Théo Zimmermann
2020-09-11[refman] Rename int to integerPierre Roux
2020-09-11[refman] Rename num to naturalPierre Roux
2020-08-25Convert ltac2 chapter to use prodn, update syntaxJim Fehrle
2020-06-08Convert Ltac chapter to prodnJim Fehrle
2020-05-16Merge PR #8855: More search optionsEmilio Jesus Gallego Arias
2020-05-15Document new Search features.Théo Zimmermann
2020-05-14Add some markers of origin.Théo Zimmermann
2020-05-14Reintroduce leftover parts; update index files; small fixes.Théo Zimmermann
2020-05-09Add a `with_strategy` tacticJason Gross
2020-05-01Remove flags, options and tables from vernac chapter.Théo Zimmermann
2020-04-28Merge PR #11718: Convert syntax extensions chapter to prodnThéo Zimmermann
2020-04-26Convert syntax extensions chapter to prodnJim Fehrle
2020-04-23Merge PR #12034: Make cumulative sprop a typing flag, deprecate command line...Pierre-Marie Pédrot
2020-04-21Document changed warnings and erros following #12038.Théo Zimmermann
2020-04-16Make cumulative sprop a typing flag, deprecate command line -sprop-cumulativeGaëtan Gilbert
2020-04-11Merge PR #11961: Convert vernac commands chapter to prodn, update syntaxThéo Zimmermann
2020-04-10Convert vernac commands chapter to prodn, update syntaxJim Fehrle
2020-04-07Fix documentation of Print Libraries following #10476.Théo Zimmermann
2020-03-29Merge PR #11944: Remove SearchAbout command, deprecated in 8.5Théo Zimmermann
2020-03-28Remove SearchAbout command, deprecated in 8.5Jim Fehrle
2020-03-28Document change of behavior of Fail in 8.11.Théo Zimmermann
2020-03-25Convert Gallina Extensions to use prodnJim Fehrle
2020-03-19Interpret the Export modifier of Set and Unset as an attribute.Théo Zimmermann
2020-03-19Document all the existing attributes.Théo Zimmermann
2020-03-18Add documentation for the export hint.Pierre-Marie Pédrot
2020-03-03[loadpath] Rework and simplify ML loadpath handlingEmilio Jesus Gallego Arias
2020-01-10missing spaceOlivier Laurent
2019-11-20Update grammar in the Terms section of Gallina chapterJim Fehrle
2019-11-06Replace "option" in doc when it refers to a flagJim Fehrle
2019-09-19Fix #10420 Add dependent evar mapping info to outputJim Fehrle
2019-09-03Add missing index for From ... Require ...Théo Zimmermann
2019-08-16Universe Checking instead of Universes CheckingSimonBoulier
2019-08-16Add documentation for typing flags.SimonBoulier
2019-07-25Remove deprecated `Backtrack` commandMaxime Dénès
2019-05-23Suggestions from review.Théo Zimmermann
2019-05-23More misc refman fixes, less undefined tokens.Théo Zimmermann
2019-05-23Define many undefined tokens, and other misc fixes.Théo Zimmermann
2019-05-22[refman] Misc fixes (mostly missing '@' signs)Clément Pit-Claudel
2019-05-22[refman] Give explicit names to the various 'Arguments' commandsClément Pit-Claudel
2019-05-19[refman] Misc fixes (indentation, whitespace, notation syntax)Clément Pit-Claudel
2019-05-16[refman] Introduce syntax for alternatives in notationsClément Pit-Claudel
2019-04-02Document the Fast Name Printing option.Pierre-Marie Pédrot
2019-02-25[Manual] Refactor documentation of internal registration commandsVincent Laporte
2019-02-25[Manual] Document primitive integersVincent Laporte
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-26 18:15:52 +0000