aboutsummaryrefslogtreecommitdiffhomepage
path: root/intf/decl_kinds.ml
Commit message (Collapse)AuthorAge
* [api] Also deprecate constructors of Decl_kinds.Gravatar Emilio Jesus Gallego Arias2017-12-23
| | | | | | | | Unfortunately OCaml doesn't deprecate the constructors of a type when the type alias is deprecated. In this case it means that we don't get rid of the kernel dependency unless we deprecate the constructors too.
* [api] Remove kernel dependency on intf (Decl_kind)Gravatar Emilio Jesus Gallego Arias2017-12-10
| | | | | | We more the `recursivity_kind` type to `Declarations`, this indeed makes sense, and now `Decl_kind` morally lives in `library` as it should.
* Remove "obsolete_locality" and fix STM vernac classification.Gravatar Maxime Dénès2017-11-29
| | | | | | | | | | We remove deprecated syntax "Coercion Local" and such, and seize the opportunity to refactor some code around vernac_expr. We also do a small fix on the STM classification, which didn't know about Let Fixpoint and Let CoFixpoint. This is a preliminary step for the work on attributes.
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
|
* Fix bugs and add an option for cumulativityGravatar Amin Timany2017-06-16
|
* Put all plugins behind an "API".Gravatar Matej Kosik2017-06-07
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-29 08:07:03 +0000