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.mli
Commit message (
Expand
)
Author
Age
*
Conv_orable made functional and part of pre_env
gareuselesinge
2013-10-31
*
enhance marshallable option for freeze (minor TODO in safe_typing)
gareuselesinge
2013-08-08
*
States: frozen states can hold closures
gareuselesinge
2013-05-06
*
code simplifications concerning Summary
letouzey
2013-04-22
*
More equality functions
ppedrot
2012-11-25
*
Updating headers.
herbelin
2012-08-08
*
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
*
New script dev/tools/change-header to automatically update Coq files headers.
herbelin
2010-06-22
*
Remove the svn-specific $Id$ annotations
letouzey
2010-04-29
*
Move from ocamlweb to ocamdoc to generate mli documentation
pboutill
2010-04-29
*
refined the conversion oracle
barras
2008-05-21
*
Compatibilité ocamlweb pour cible doc
herbelin
2005-01-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
*
reparation de make doc (ocamlweb & _)
letouzey
2001-12-19
*
nouvel algo de conversion plus uniforme
barras
2001-11-29