aboutsummaryrefslogtreecommitdiff
path: root/library/kindops.ml
AgeCommit message (Expand)Author
2016-07-03errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...Pierre Letouzey
2016-01-20Update copyright headers.Maxime Dénès
2015-01-12Update headers.Maxime Dénès
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
2013-01-28Uniformization of the "anomaly" command.ppedrot
2012-08-08Updating headers.herbelin
2012-05-29Decl_kinds becomes a pure mli file, remaining ops in new file kindops.mlletouzey