index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
kernel
/
conv_oracle.mli
Age
Commit message (
Expand
)
Author
2018-11-19
Rename TranspState into TransparentState.
Pierre-Marie Pédrot
2018-11-19
Move transparent_state to its own module.
Pierre-Marie Pédrot
2018-02-27
Update headers following #6543.
Théo Zimmermann
2017-11-06
[api] Deprecate all legacy uses of Names in core.
Emilio Jesus Gallego Arias
2017-07-04
Bump year in headers.
Pierre-Marie Pédrot
2016-01-20
Update copyright headers.
Maxime Dénès
2015-01-15
Correct restriction of vm_compute when handling universe polymorphic
Matthieu Sozeau
2015-01-12
Update headers.
Maxime Dénès
2014-05-06
This commit adds full universe polymorphism and fast projections to Coq.
Matthieu Sozeau
2014-03-19
Adding a Print Strategy vernacular command. It allows to check the
Pierre-Marie Pédrot
2013-10-31
Conv_orable made functional and part of pre_env
gareuselesinge
2013-08-08
enhance marshallable option for freeze (minor TODO in safe_typing)
gareuselesinge
2013-05-06
States: frozen states can hold closures
gareuselesinge
2013-04-22
code simplifications concerning Summary
letouzey
2012-11-25
More equality functions
ppedrot
2012-08-08
Updating headers.
herbelin
2011-08-10
Propagated information from the reduction tactics to the kernel so
herbelin
2010-07-24
Updated all headers for 8.3 and trunk
herbelin
2010-06-22
New script dev/tools/change-header to automatically update Coq files headers.
herbelin
2010-04-29
Remove the svn-specific $Id$ annotations
letouzey
2010-04-29
Move from ocamlweb to ocamdoc to generate mli documentation
pboutill
2008-05-21
refined the conversion oracle
barras
2005-01-21
Compatibilité ocamlweb pour cible doc
herbelin
2004-11-16
IMPORTANT COMMIT: constant is now an ADT (it used to be equal to kernel_name).
sacerdot
2004-10-20
COMMITED BYTECODE COMPILER
barras
2004-07-16
Nouvelle en-tête
herbelin
2004-06-02
Fusion comparaison Const/Var; export is_opaque
herbelin
2002-08-02
Modules dans COQ\!\!\!\!
coq
2001-12-19
reparation de make doc (ocamlweb & _)
letouzey
2001-11-29
nouvel algo de conversion plus uniforme
barras