aboutsummaryrefslogtreecommitdiff
path: root/vernac/declareInd.mli
AgeCommit message (Expand)Author
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