aboutsummaryrefslogtreecommitdiffhomepage
path: root/intf/decl_kinds.mli
Commit message (Expand)AuthorAge
* COMMENT: unfortunatelly, ocamldoc does not recognize this kind of markup: it ...Gravatar Matej Kosik2016-10-27
* Revert "Merge remote-tracking branch 'github/pr/283' into trunk"Gravatar Maxime Dénès2016-09-22
* Rename Decl_kinds.binding_kind into Decls_kind.implicit_status.Gravatar Maxime Dénès2016-09-20
* Stylistic improvements in intf/decl_kinds.mli.Gravatar Maxime Dénès2016-09-20
* Update copyright headers.Gravatar Maxime Dénès2016-01-20
* Update headers.Gravatar Maxime Dénès2015-01-12
* Adapt Y. Bertot's path on private inductives (now the keyword is "Private").Gravatar Yves Bertot2014-05-06
* This commit adds full universe polymorphism and fast projections to Coq.Gravatar Matthieu Sozeau2014-05-06
* Added a Local Definition vernacular command. This type of definitionGravatar ppedrot2013-03-11
* Updating headers.Gravatar herbelin2012-08-08
* locus.mli for occurrences+clauses, misctypes.mli for various little thingsGravatar letouzey2012-05-29
* Decl_kinds becomes a pure mli file, remaining ops in new file kindops.mlGravatar letouzey2012-05-29
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-04 22:00:23 +0000