aboutsummaryrefslogtreecommitdiff
path: root/vernac/comProgramFixpoint.mli
AgeCommit message (Expand)Author
2020-11-26[vernac] Allow to control typing flags with attributes.Emilio Jesus Gallego Arias
2020-11-02attribute #[using] for Definition and FixpointEnrico Tassi
2020-07-08[obligations] Functionalize Program stateEmilio Jesus Gallego Arias
2020-06-26[declare] [api] Removal of duplicated type aliases.Emilio Jesus Gallego Arias
2020-05-07[declare] Merge DeclareDef into DeclareEmilio Jesus Gallego Arias
2020-03-18Update headers in the whole code base.Théo Zimmermann
2019-07-23[vernacexpr] Remove duplicate fixpoint record.Emilio Jesus Gallego Arias
2019-07-23[vernacexpr] Refactor fixpoint AST.Emilio Jesus Gallego Arias
2019-06-24[api] Move `locality` from `library` to `vernac`.Emilio Jesus Gallego Arias
2019-06-24[lemmas] [proof] Split proof kinds into per-layer components.Emilio Jesus Gallego Arias
2017-12-17[vernac] Split `command.ml` into separate files.Emilio Jesus Gallego Arias