aboutsummaryrefslogtreecommitdiff
path: root/doc/tools/docgram/fullGrammar
AgeCommit message (Expand)Author
2020-06-08Convert Ltac chapter to prodnJim Fehrle
2020-05-15Document new Search features.Théo Zimmermann
2020-05-15Update docgram following #12122 and #12229.Théo Zimmermann
2020-05-09Add a `with_strategy` tacticJason Gross
2020-04-21Update common.edit_mlg and fullGrammar following #12038.Théo Zimmermann
2020-04-13Update syntax of Import / Export in documentation.Théo Zimmermann
2020-04-07Support universe bindings and universe constraints in Let definitions.Théo Zimmermann
2020-03-28Remove SearchAbout command, deprecated in 8.5Jim Fehrle
2020-03-25Convert Gallina Extensions to use prodnJim Fehrle
2020-03-19Update fullGrammar, common.edit_mlg and orderedGrammar...Théo Zimmermann
2020-03-19Update fullGrammar and common.edit_mlg following #11839.Théo Zimmermann
2020-03-09Remove some productionlistsJim Fehrle
2020-02-28Convert Gallina Vernac to use prodnJim Fehrle
2019-12-28Convert productionlists to prodnsJim Fehrle
2019-11-20Update grammar in the Terms section of Gallina chapterJim Fehrle
2019-07-19Introduce doc_gram, a utilty for extracting Coq's grammar from .mlg filesJim Fehrle