index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
kernel
/
conv_oracle.ml
Commit message (
Expand
)
Author
Age
*
Bump year in headers.
Pierre-Marie Pédrot
2017-07-04
*
[cleanup] Unify all calls to the error function.
Emilio Jesus Gallego Arias
2017-05-27
*
errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...
Pierre Letouzey
2016-07-03
*
Update copyright headers.
Maxime Dénès
2016-01-20
*
Fix detection of ties in oracle_order.
Guillaume Melquiond
2015-10-15
*
Correct restriction of vm_compute when handling universe polymorphic
Matthieu Sozeau
2015-01-15
*
Update headers.
Maxime Dénès
2015-01-12
*
Fixing the previous patch to keep transparent states in sync.
Pierre-Marie Pédrot
2014-07-09
*
Recovering transparent state from kernel oracles in constant time.
Pierre-Marie Pédrot
2014-07-09
*
Adding a Print Strategy vernacular command. It allows to check the
Pierre-Marie Pédrot
2014-03-19
*
Conv_orable made functional and part of pre_env
gareuselesinge
2013-10-31
*
Removing some generic equalities.
ppedrot
2013-10-22
*
States: frozen states can hold closures
gareuselesinge
2013-05-06
*
code simplifications concerning Summary
letouzey
2013-04-22
*
Modulification of identifier
ppedrot
2012-12-14
*
More equality functions
ppedrot
2012-11-25
*
Updating headers.
herbelin
2012-08-08
*
Noise for nothing
pboutill
2012-03-02
*
Propagated information from the reduction tactics to the kernel so
herbelin
2011-08-10
*
Updated all headers for 8.3 and trunk
herbelin
2010-07-24
*
Added a few informations about file lineages (for the most part in kernel)
herbelin
2010-05-09
*
Remove the svn-specific $Id$ annotations
letouzey
2010-04-29
*
Some dead code removal + cleanups
letouzey
2009-04-08
*
refined the conversion oracle
barras
2008-05-21
*
IMPORTANT COMMIT: constant is now an ADT (it used to be equal to kernel_name).
sacerdot
2004-11-16
*
COMMITED BYTECODE COMPILER
barras
2004-10-20
*
Nouvelle en-tête
herbelin
2004-07-16
*
Fusion comparaison Const/Var; export is_opaque
herbelin
2004-06-02
*
Modules dans COQ\!\!\!\!
coq
2002-08-02
*
nouvel algo de conversion plus uniforme
barras
2001-11-29