index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
library
/
library.mllib
Commit message (
Expand
)
Author
Age
*
Assumptions: more informative print for False axiom (Close: #4054)
Enrico Tassi
2015-06-29
*
Index keys instead of simply global references.
Matthieu Sozeau
2014-09-27
*
First version of keyed subterm selection in unification.
Matthieu Sozeau
2014-09-27
*
This commit adds full universe polymorphism and fast projections to Coq.
Matthieu Sozeau
2014-05-06
*
Moved the Loadpath part of Library to its own file, and documented
ppedrot
2013-03-26
*
correct some ends of .mllib files (avoid a broken tolink.ml)
letouzey
2012-08-24
*
global_reference migrated from Libnames to new Globnames, less deps in gramma...
letouzey
2012-05-29
*
Decl_kinds becomes a pure mli file, remaining ops in new file kindops.ml
letouzey
2012-05-29
*
First attempt at making Print Assumption compatible with opaque modules (fix ...
letouzey
2011-10-25
*
Delete trailing whitespaces in all *.{v,ml*} files
glondu
2009-09-17
*
Many changes in the Makefile infrastructure + a beginning of ocamlbuild
letouzey
2009-03-20