index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
kernel
/
declareops.ml
Commit message (
Expand
)
Author
Age
...
*
Adapt Y. Bertot's path on private inductives (now the keyword is "Private").
Yves Bertot
2014-05-06
*
- Rename eq to equal in Univ, document new modules, set interfaces.
Matthieu Sozeau
2014-05-06
*
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
*
Fixing pervasive equalities. In particular, I removed the code that deleted
Pierre-Marie Pédrot
2014-03-03
*
Lazyconstr -> Opaqueproof
Enrico Tassi
2014-02-26
*
New compilation mode -vi2vo
Enrico Tassi
2014-02-26
*
Revert "Partial revert of r16711"
Maxime Dénès
2013-12-28
*
Removing native_name reference from constant_body.
Maxime Dénès
2013-12-28
*
STM: capture type checking error (Closes: 3195)
Enrico Tassi
2013-12-24
*
Future: better doc + restore ~pure optimization
gareuselesinge
2013-10-31
*
Future: ported to Ephemeron + exception enhancing
gareuselesinge
2013-10-18
*
Removing a bunch of generic equalities.
ppedrot
2013-09-27
*
ind_tables: properly handling side effects
gareuselesinge
2013-08-30
*
Partial revert of r16711
letouzey
2013-08-20
*
Declareops + Modops : more clever substitutions
letouzey
2013-08-20
*
Attempt to restore hash-consing of opaque terms
letouzey
2013-08-20
*
abstract+Defined: create opaque sub proofs (as pre-ParalITP)
gareuselesinge
2013-08-19
*
enhance marshallable option for freeze (minor TODO in safe_typing)
gareuselesinge
2013-08-08
*
State Transaction Machine
gareuselesinge
2013-08-08
*
Merging Context and Sign.
ppedrot
2013-04-29
*
Revised infrastructure for lazy loading of opaque proofs
letouzey
2013-04-02
*
kernel/declarations becomes a pure mli
letouzey
2013-02-26
[prev]