aboutsummaryrefslogtreecommitdiff
path: root/checker/safe_typing.mli
AgeCommit message (Expand)Author
2018-11-06[checker] Refactor by sharing code with the kernelMaxime Dénès
2018-02-27Update headers following #6543.Théo Zimmermann
2017-07-04Bump year in headers.Pierre-Marie Pédrot
2016-01-20Update copyright headers.Maxime Dénès
2015-11-04Checker was forgetting to register global universes introduced by opaqueMatthieu Sozeau
2015-01-12Update headers.Maxime Dénès
2014-03-11vi2vo: universes handling finally fixedEnrico Tassi
2014-03-05Remove many superfluous 'open' indicated by ocamlc -w +33Pierre Letouzey
2013-04-15Checker: vo validation is now done in check.ml (and always)letouzey
2013-04-15Checker: reified encoding of .vo types in values.mlletouzey
2013-04-15Checker: regroup all vo-related types in cic.mliletouzey
2013-04-02Revised infrastructure for lazy loading of opaque proofsletouzey
2012-08-08Updating headers.herbelin
2012-04-12lib directory is cut in 2 cma.pboutill
2011-04-03Lazy loading of opaque proofs: fast as -dont-load-proofs without its drawbacksletouzey
2010-09-24Checker: remove some dead codeletouzey
2010-08-27* checker/Safe_typing.LightenLibrary:regisgia
2010-08-27* Improve documentation of LightenLibrary.regisgia
2010-08-27* (checker|kernel)/Safe_typing: New LightenLibrary.regisgia
2010-07-24Updated all headers for 8.3 and trunkherbelin
2010-04-29Remove the svn-specific $Id$ annotationsletouzey
2008-05-06checker deals with polymorphic constants and module aliasesbarras
2008-04-21added the .vo checker (with independent Makefile)barras
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 14:41:08 +0000