aboutsummaryrefslogtreecommitdiffhomepage
path: root/library/library.mllib
Commit message (Expand)AuthorAge
* [api] Miscellaneous consolidation + moves to engine.Gravatar Emilio Jesus Gallego Arias2017-11-21
* Move univops from kernel to libraryGravatar Amin Timany2017-06-16
* [coqlib] Move `Coqlib` to `library/`.Gravatar Emilio Jesus Gallego Arias2017-05-27
* Moving Universes to the engine/ folder.Gravatar Pierre-Marie Pédrot2016-10-30
* Assumptions: more informative print for False axiom (Close: #4054)Gravatar Enrico Tassi2015-06-29
* Index keys instead of simply global references.Gravatar Matthieu Sozeau2014-09-27
* First version of keyed subterm selection in unification.Gravatar Matthieu Sozeau2014-09-27
* This commit adds full universe polymorphism and fast projections to Coq.Gravatar Matthieu Sozeau2014-05-06
* Moved the Loadpath part of Library to its own file, and documentedGravatar ppedrot2013-03-26
* correct some ends of .mllib files (avoid a broken tolink.ml)Gravatar letouzey2012-08-24
* global_reference migrated from Libnames to new Globnames, less deps in gramma...Gravatar letouzey2012-05-29
* Decl_kinds becomes a pure mli file, remaining ops in new file kindops.mlGravatar letouzey2012-05-29
* First attempt at making Print Assumption compatible with opaque modules (fix ...Gravatar letouzey2011-10-25
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
* Many changes in the Makefile infrastructure + a beginning of ocamlbuildGravatar letouzey2009-03-20