aboutsummaryrefslogtreecommitdiff
path: root/library/kindops.mli
AgeCommit message (Collapse)Author
2019-07-01[api] Refactor most of `Decl_kinds`Emilio Jesus Gallego Arias
We move the bulk of `Decl_kinds` to a better place [namely `interp/decls`] and refactor the use of this information quite a bit. The information seems to be used almost only for `Dumpglob`, so it certainly should end there to achieve a cleaner core. Note the previous commits, as well as the annotations regarding the dubious use of the "variable" data managed by the `Decls` file. IMO this needs more work, but this should be a good start.
2019-06-17Update ml-style headers to new year.Théo Zimmermann
2018-02-27Update headers following #6543.Théo Zimmermann
2017-11-29Remove "obsolete_locality" and fix STM vernac classification.Maxime Dénès
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.
2017-07-04Bump year in headers.Pierre-Marie Pédrot
2016-01-20Update copyright headers.Maxime Dénès
2015-01-12Update headers.Maxime Dénès
2013-05-09Cosmetic changegareuselesinge
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16501 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-08-08Updating headers.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15715 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-05-29Decl_kinds becomes a pure mli file, remaining ops in new file kindops.mlletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15368 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 17:37:53 +0000