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