aboutsummaryrefslogtreecommitdiffhomepage
path: root/library/kindops.ml
Commit message (Expand)AuthorAge
* Drop '.' from CErrors.anomaly, insert it in argsGravatar Jason Gross2017-06-02
* Revert "Merge remote-tracking branch 'github/pr/283' into trunk"Gravatar Maxime Dénès2016-09-22
* Stylistic improvements in intf/decl_kinds.mli.Gravatar Maxime Dénès2016-09-20
* errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...Gravatar Pierre Letouzey2016-07-03
* Update copyright headers.Gravatar Maxime Dénès2016-01-20
* Update headers.Gravatar Maxime Dénès2015-01-12
* 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
* 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