index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
kernel
/
opaqueproof.mli
Age
Commit message (
Expand
)
Author
2019-05-27
Remove the delayed universe table from object files.
Pierre-Marie Pédrot
2019-05-24
Remove the indirect opaque accessor hooks from Opaqueproof.
Pierre-Marie Pédrot
2019-05-24
Statically ensure the content of delayed proofs in vio file.
Pierre-Marie Pédrot
2019-05-24
Remove a useless call to the Future API for opaque proofs in the STM.
Pierre-Marie Pédrot
2019-05-24
Remove a last use of opacity-piercing function in Safe_typing.
Pierre-Marie Pédrot
2019-05-20
Do not perform the section variable check on global recipes.
Pierre-Marie Pédrot
2019-05-20
Ensure statically that declarations built by Term_typing are direct.
Pierre-Marie Pédrot
2019-05-14
Reduce the attack surface of Opaqueproof.
Pierre-Marie Pédrot
2018-06-27
Swapping Context and Constr: defining declarations on constr in Constr.
Hugo Herbelin
2018-02-27
Update headers following #6543.
Théo Zimmermann
2017-12-30
Returning instance instead of substitution in universe context abstraction.
Pierre-Marie Pédrot
2017-11-06
[api] Move structures deprecated in the API to the core.
Emilio Jesus Gallego Arias
2017-07-04
Bump year in headers.
Pierre-Marie Pédrot
2017-06-16
Clean up universes of constants and inductives
Amin Timany
2017-03-27
Fix hashconsing of terms in the kernel.
Pierre-Marie Pédrot
2016-01-21
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-01-20
Update copyright headers.
Maxime Dénès
2016-01-11
CLEANUP: kernel/context.ml{,i}
Matej Kosik
2015-12-07
Fix some typos.
Guillaume Melquiond
2015-02-02
Removing dead code.
Pierre-Marie Pédrot
2015-01-12
Update headers.
Maxime Dénès
2014-10-13
library/opaqueTables: enable their use in interactive mode
Enrico Tassi
2014-08-03
Move to a representation of universe polymorphic constants using indices for ...
Matthieu Sozeau
2014-05-06
- Fix bug preventing apply from unfolding Fixpoints.
Matthieu Sozeau
2014-05-06
Adapt universe polymorphic branch to new handling of futures for delayed proofs.
Matthieu Sozeau
2014-05-06
This commit adds full universe polymorphism and fast projections to Coq.
Matthieu Sozeau
2014-02-26
Lazyconstr -> Opaqueproof
Enrico Tassi
