aboutsummaryrefslogtreecommitdiff
path: root/intf/decl_kinds.mli
AgeCommit message (Expand)Author
2017-06-07Put all plugins behind an "API".Matej Kosik
2016-10-27COMMENT: unfortunatelly, ocamldoc does not recognize this kind of markup: it ...Matej Kosik
2016-09-22Revert "Merge remote-tracking branch 'github/pr/283' into trunk"Maxime Dénès
2016-09-20Rename Decl_kinds.binding_kind into Decls_kind.implicit_status.Maxime Dénès
2016-09-20Stylistic improvements in intf/decl_kinds.mli.Maxime Dénès
2016-01-20Update copyright headers.Maxime Dénès
2015-01-12Update headers.Maxime Dénès
2014-05-06Adapt Y. Bertot's path on private inductives (now the keyword is "Private").Yves Bertot
2014-05-06This commit adds full universe polymorphism and fast projections to Coq.Matthieu Sozeau
2013-03-11Added a Local Definition vernacular command. This type of definitionppedrot
2012-08-08Updating headers.herbelin
2012-05-29locus.mli for occurrences+clauses, misctypes.mli for various little thingsletouzey
2012-05-29Decl_kinds becomes a pure mli file, remaining ops in new file kindops.mlletouzey
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-07 07:25:49 +0000