aboutsummaryrefslogtreecommitdiffhomepage
path: root/library/kindops.ml
Commit message (Expand)AuthorAge
* Added a Local Definition vernacular command. This type of definitionGravatar ppedrot2013-03-11
* Uniformization of the "anomaly" command.Gravatar ppedrot2013-01-28
* Updating headers.Gravatar herbelin2012-08-08
* Decl_kinds becomes a pure mli file, remaining ops in new file kindops.mlGravatar letouzey2012-05-29