aboutsummaryrefslogtreecommitdiffhomepage
path: root/intf/decl_kinds.mli
Commit message (Expand)AuthorAge
* 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