aboutsummaryrefslogtreecommitdiff
path: root/vernac/declareInd.ml
AgeCommit message (Expand)Author
2021-03-26[recordops] complete API rewrite; the module is now called [structures]Enrico Tassi
2020-11-26[vernac] Allow to control typing flags with attributes.Emilio Jesus Gallego Arias
2020-04-17Merge PR #11135: Simplifying the code declaring the constants bound to primit...Pierre-Marie Pédrot
2020-04-13correctly open objects for Names filtersGaëtan Gilbert
2020-04-13pass filters aroundGaëtan Gilbert
2020-04-13Simplifying the declaration of constants bound to primitive projections.Hugo Herbelin
2020-03-18Update headers in the whole code base.Théo Zimmermann
2019-12-22Remove the hacks relying on hardwired libobject tags.Pierre-Marie Pédrot
2019-10-25[inductive] [declare] Move full inductive declaration to declareIndEmilio Jesus Gallego Arias
2019-10-24[declare] Split inductive declaration code to vernac/Emilio Jesus Gallego Arias