aboutsummaryrefslogtreecommitdiff
path: root/vernac/declareUniv.ml
AgeCommit message (Expand)Author
2020-05-07[declare] Merge DeclareDef into DeclareEmilio Jesus Gallego Arias
2020-04-21[declare] [tactics] Move declare to `vernac`Emilio Jesus Gallego Arias
2020-04-13pass filters aroundGaëtan Gilbert
2020-03-18Update headers in the whole code base.Théo Zimmermann
2020-01-21Typo in an anomaly message.Hugo Herbelin
2019-10-24[declare] Split universe declaration code to vernac/Emilio Jesus Gallego Arias