aboutsummaryrefslogtreecommitdiffhomepage
path: root/checker/safe_typing.ml
Commit message (Expand)AuthorAge
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
* [cleanup] Unify all calls to the error function.Gravatar Emilio Jesus Gallego Arias2017-05-27
* Merge PR #244.Gravatar Pierre-Marie Pédrot2016-09-08
|\
| * Make the user_err header an optional parameter.Gravatar Emilio Jesus Gallego Arias2016-08-19
| * Remove errorlabstrm in favor of user_errGravatar Emilio Jesus Gallego Arias2016-08-19
|/
* errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...Gravatar Pierre Letouzey2016-07-03
* Fixing the checker.Gravatar Pierre-Marie Pédrot2016-06-18
* Feedback cleanupGravatar Emilio Jesus Gallego Arias2016-05-31
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-21
|\
| * Update copyright headers.Gravatar Maxime Dénès2016-01-20
* | Do not compose "str" and "to_string" whenever possible.Gravatar Guillaume Melquiond2015-12-22
|/
* Checker was forgetting to register global universes introduced by opaqueGravatar Matthieu Sozeau2015-11-04
* Univs: update checkerGravatar Matthieu Sozeau2015-10-02
* Option -type-in-type: added support in checker and making it contaminatingGravatar Hugo Herbelin2015-07-10
* coqchk: more prints when -debugGravatar Enrico Tassi2015-03-23
* Update headers.Gravatar Maxime Dénès2015-01-12
* vi2vo: universes handling finally fixedGravatar Enrico Tassi2014-03-11
* Remove many superfluous 'open' indicated by ocamlc -w +33Gravatar Pierre Letouzey2014-03-05
* Checker: vo validation is now done in check.ml (and always)Gravatar letouzey2013-04-15
* Checker: reified encoding of .vo types in values.mlGravatar letouzey2013-04-15
* Checker: regroup all vo-related types in cic.mliGravatar letouzey2013-04-15
* Revised infrastructure for lazy loading of opaque proofsGravatar letouzey2013-04-02
* Safe_typing+Libary: use some arrays instead of lists in vo structuresGravatar letouzey2013-03-28
* Dir_path --> DirPathGravatar letouzey2013-02-19
* Modulification of dir_pathGravatar ppedrot2012-12-14
* Updating headers.Gravatar herbelin2012-08-08
* Getting rid of Pp.msgnl and Pp.message.Gravatar ppedrot2012-06-01
* Noise for nothingGravatar pboutill2012-03-02
* Lazy loading of opaque proofs: fast as -dont-load-proofs without its drawbacksGravatar letouzey2011-04-03
* Checker: remove some dead codeGravatar letouzey2010-09-24
* Explicit Mod_checking signatureGravatar glondu2010-09-16
* Sharing is not anymore broken by traverse_module.Gravatar soubiran2010-09-15
* * checker/Safe_typing.LightenLibrary:Gravatar regisgia2010-08-27
* * (checker|kernel)/Safe_typing:Gravatar regisgia2010-08-27
* * (checker|kernel)/Safe_typing:Gravatar regisgia2010-08-27
* * checker/SafeTyping kernel/SafeTyping:Gravatar regisgia2010-08-27
* * Improve documentation of LightenLibrary.Gravatar regisgia2010-08-27
* * (checker|kernel)/Safe_typing: New LightenLibrary.Gravatar regisgia2010-08-27
* adpated the checker to handle coomutative cuts and lazynessGravatar barras2010-07-30
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
* kills a warning about vo in checker/safe_typingGravatar letouzey2010-03-18
* [checker] fixed vo validation problems, module incompatibilities remainGravatar barras2010-02-19
* This big commit addresses two problems:Gravatar soubiran2009-10-21
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
* porting r11900 11905 and 11953 to trunkGravatar barras2009-03-02
* fixed bug #1927 + univ constraints (module cstrs include cstrs of its subcomp...Gravatar barras2008-09-02
* doc of coqchk + improved module cache and computation of module setsGravatar barras2008-05-23
* checker deals with polymorphic constants and module aliasesGravatar barras2008-05-06
* added the .vo checker (with independent Makefile)Gravatar barras2008-04-21