aboutsummaryrefslogtreecommitdiff
path: root/doc/sphinx/proof-engine/vernacular-commands.rst
AgeCommit message (Expand)Author
2021-03-08Convert 2nd part of rewriting chapter to prodnJim Fehrle
2021-02-24Infrastructure for fine-grained debug flagsMaxime Dénès
2021-02-08Properly document the local and global locality attributes.Théo Zimmermann
2021-01-25Remove the SearchHead commandJim Fehrle
2020-12-30Convert rewriting and proof-mode chapters to prodnJim Fehrle
2020-11-26[attributes] [typing] Rename `typing` to `bypass_check`Emilio Jesus Gallego Arias
2020-11-26[attributes] [doc] Documentation review by Théo.Emilio Jesus Gallego Arias
2020-11-26[vernac] Allow to control typing flags with attributes.Emilio Jesus Gallego Arias
2020-11-24Convert auto chapter to prodnJim Fehrle
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