aboutsummaryrefslogtreecommitdiff
path: root/vernac/comHints.ml
AgeCommit message (Expand)Author
2020-06-26[declare] [api] Removal of duplicated type aliases.Emilio Jesus Gallego Arias
2020-05-10No more local reduction functions in Reductionops.Pierre-Marie Pédrot
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-21[hints] Move and split Hint Declaration AST to vernacEmilio Jesus Gallego Arias