aboutsummaryrefslogtreecommitdiff
path: root/vernac/g_vernac.mlg
AgeCommit message (Expand)Author
2020-05-18[search] [ssr] Emit deprecated message when calling search from ssreflectEmilio Jesus Gallego Arias
2020-05-15Search: new clauses for searching head, conclusion, kind...Hugo Herbelin
2020-05-13Merge PR #12229: Hopefully consensual cleaning of keywordsThéo Zimmermann
2020-05-09Add a `with_strategy` tacticJason Gross
2020-05-09Merge PR #12122: Avoid registering as keywords the #... in PrimitiveMaxime Dénès
2020-05-06Stop keeping outdated static list of keywords.Hugo Herbelin
2020-04-22Remove # keywords in PrimitivePierre Roux
2020-04-20Move new iter_table function to Goptions.Théo Zimmermann
2020-04-13Partial import inductive(..)Gaëtan Gilbert
2020-04-13syntax for import filtersGaëtan Gilbert
2020-04-07Support universe bindings and universe constraints in Let definitions.Théo Zimmermann
2020-04-05Fixes #11194 (Canonical/Coercion not located for coqdoc).Hugo Herbelin
2020-04-02Remove Chapter command.Théo Zimmermann
2020-03-31Merge PR #11668: Helping issue #11659 by leaving only the Cast hack in the gr...Maxime Dénès
2020-03-28Remove SearchAbout command, deprecated in 8.5Jim Fehrle
2020-03-27Helping issue #11659 by leaving only the Cast hack in the grammar.Hugo Herbelin
2020-03-19Make Cumulative, NonCumulative and Private attributes.Théo Zimmermann
2020-03-18Update headers in the whole code base.Théo Zimmermann
2020-03-04Experimenting using a record for decl_notation.Hugo Herbelin
2020-03-04Adding support for an "only parsing" modifier in "where"-based notations.Hugo Herbelin
2020-03-03[vernac] Use a record for VernacAddLoadPathEmilio Jesus Gallego Arias
2020-03-03[loadpath] Rework and simplify ML loadpath handlingEmilio Jesus Gallego Arias
2020-03-01Refactor lookaheads using DSLMaxime Dénès
2020-02-23Fix #11654: syntax of inductive declaration.Théo Zimmermann
2020-02-19Merge PR #11636: Revert buggy commit mistakenly pushed with #11530Emilio Jesus Gallego Arias
2020-02-19Merge PR #11600: New syntax [Inductive Acc A R | x : Prop := ...]Emilio Jesus Gallego Arias
2020-02-19Revert "Granting #9516 and #9518 (support for numerals and strings in custom ...Hugo Herbelin
2020-02-17New syntax [Inductive Acc A R | x : Prop := ...]Gaëtan Gilbert
2020-02-16Granting #9516 and #9518 (support for numerals and strings in custom entries).Hugo Herbelin
2020-02-16Mini-factorization in vernac grammar.Hugo Herbelin
2020-02-15Reorganize type "production_level" along a more intuitive structure.Hugo Herbelin
2020-02-13Don't duplicate the inductive keyword for each block elt when parsingGaëtan Gilbert
2020-02-04Add syntax for non maximally inserted implicit argumentsSimonBoulier
2020-01-09Merge PR #11164: [CS] allow Let variable to be canonicalPierre-Marie Pédrot
2019-12-28Extend `Print Canonical Projections` with a search functionalityKazuhiko Sakaguchi
2019-12-24[Attributes] accept #[canonical] (Let|Definition)Enrico Tassi
2019-12-02Remove deprecated compat modifier of Notation / Infix commands.Théo Zimmermann
2019-11-30Actually deprecate `SearchAbout`Maxime Dénès
2019-11-27Remove deprecated commands `AddPath`, `AddRecPath` and `DelPath`Maxime Dénès
2019-11-27[release] Update files for 8.12 release per release process.Emilio Jesus Gallego Arias
2019-11-25Merge PR #11146: Combine similar arguments when printing Arguments commandHugo Herbelin
2019-11-21[coq] Untabify the whole ML codebase.Emilio Jesus Gallego Arias
2019-11-20make VernacArguments closer to user syntaxGaëtan Gilbert
2019-11-19G_constr: Renaming record_fields_instance -> fields_def.Hugo Herbelin
2019-11-19Grammar: mini-factorization between fix/cofix and Fixpoint/CoFixpoint.Hugo Herbelin
2019-11-15Merge PR #11079: Rename non-unique local nonterminalsHugo Herbelin
2019-11-14Rename non-unique local nonterminalsJim Fehrle
2019-11-11Run update-compat script with --release option.Théo Zimmermann
2019-11-01Add "==", "<", "<=" in PrimFloat.vErik Martin-Dorel
2019-11-01Add next_{up,down} primitive float functionsPierre Roux
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 12:18:36 +0000