index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
library
/
assumptions.ml
Commit message (
Expand
)
Author
Age
*
Initial work on reintroducing old-style polymorphism for compatibility (the s...
Matthieu Sozeau
2014-05-06
*
This commit adds full universe polymorphism and fast projections to Coq.
Matthieu Sozeau
2014-05-06
*
Declarations.mli: reorganization of modular structures
letouzey
2013-08-20
*
Revised infrastructure for lazy loading of opaque proofs
letouzey
2013-04-02
*
kernel/declarations becomes a pure mli
letouzey
2013-02-26
*
Names: revised representation of constants and mutual_inductive
letouzey
2013-02-19
*
Uniformization of the "anomaly" command.
ppedrot
2013-01-28
*
Modulification of Label
ppedrot
2012-12-18
*
Modulification of identifier
ppedrot
2012-12-14
*
Monomorphization (library)
ppedrot
2012-11-22
*
Fixed #2926:
ppedrot
2012-10-29
*
Partial revert of Yann commit in order to use CLib.List when opening
ppedrot
2012-09-14
*
This patch removes unused "open" (automatically generated from
regisgia
2012-09-14
*
Updating headers.
herbelin
2012-08-08
*
Module names and constant/inductive names are now in two separate namespaces
letouzey
2012-03-26
*
Noise for nothing
pboutill
2012-03-02
*
First attempt at making Print Assumption compatible with opaque modules (fix ...
letouzey
2011-10-25