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
*
[api] Remove Misctypes.
Emilio Jesus Gallego Arias
2018-06-12
*
[api] Relocate `intf` modules according to dependency-order.
Emilio Jesus Gallego Arias
2018-04-23
*
[api] Miscellaneous consolidation + moves to engine.
Emilio Jesus Gallego Arias
2017-11-21
*
Move univops from kernel to library
Amin Timany
2017-06-16
*
[coqlib] Move `Coqlib` to `library/`.
Emilio Jesus Gallego Arias
2017-05-27
*
Moving Universes to the engine/ folder.
Pierre-Marie Pédrot
2016-10-30
*
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