aboutsummaryrefslogtreecommitdiffhomepage
path: root/checker
Commit message (Expand)AuthorAge
* Getting rid of Pp.msgGravatar ppedrot2012-05-30
* More uniformisation in Pp.warn functions.Gravatar ppedrot2012-05-30
* remove many excessive open Util & Errors in mli'sGravatar letouzey2012-05-29
* lib directory is cut in 2 cma.Gravatar pboutill2012-04-12
* Adapt the checker after commit 15080Gravatar letouzey2012-03-26
* Module names and constant/inductive names are now in two separate namespacesGravatar letouzey2012-03-26
* Univ: enforce_leq instead of enforce_geq for more uniformityGravatar letouzey2012-03-22
* Noise for nothingGravatar pboutill2012-03-02
* Add support for XDG_DATA_HOME and XDG_DATA_DIRS.Gravatar pboutill2011-11-20
* Checker/subtyping.ml: avoid adding in env a module already there (fix #2609)Gravatar letouzey2011-10-26
* More descriptive error messages in checkerGravatar glondu2011-10-20
* Esubst: make types of substitutions & lifts privateGravatar puech2011-08-08
* bug 2423: consider "" as the empty prefixGravatar barras2011-07-07
* fixed coqchk usage and man page + added option -coqlibGravatar barras2011-07-07
* ported r14149 from v8.3 branch: bug in checker (redefined global)Gravatar barras2011-05-23
* Modops: the strengthening functions can work without any env argumentGravatar letouzey2011-05-17
* Add directories in COQPATH to search path.Gravatar herbelin2011-04-14
* Reorder search path order, so the standard library is search last.Gravatar herbelin2011-04-14
* Subtyping: align coqtop behavior concerning opaque csts on coqchk's oneGravatar letouzey2011-04-12
* Lazy loading of opaque proofs: fast as -dont-load-proofs without its drawbacksGravatar letouzey2011-04-03
* checker: cleanupGravatar glondu2011-03-04
* checker: add eta-expansionGravatar glondu2011-03-04
* Propagate recent kernel changes to the checkerGravatar letouzey2011-03-03
* - Use transparency information all the way through unification andGravatar msozeau2011-02-17
* A fine-grain control of inlining at functor application via priority levelsGravatar letouzey2011-01-31
* Univ.constraints made fully abstract instead of being a Set of abstract stuffGravatar letouzey2010-12-18
* Fix function applications without labels (OCaml warning 6)Gravatar glondu2010-09-28
* Checker: remove some dead codeGravatar letouzey2010-09-24
* Some dead code removal, thanks to Oug analyzerGravatar letouzey2010-09-24
* Fix inconsistency in Prop/Set conversion checkGravatar glondu2010-09-23
* Explicit Mod_checking signatureGravatar glondu2010-09-16
* Sharing is not anymore broken by traverse_module.Gravatar soubiran2010-09-15
* Fix likely semantic typosGravatar glondu2010-09-15
* Fix unescaped end-of-lines (OCaml warning 29)Gravatar glondu2010-09-13
* * 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
* * lib/Flags: Replace dont_load_proofs by load_proofs since not loadingGravatar 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
* ported bug fix r13290 to checkerGravatar barras2010-07-22
* Fix typosGravatar glondu2010-06-02
* Cleanup: remove code specific for ocaml 3.06Gravatar letouzey2010-06-01
* Add (almost) compatibility with camlp4, without breaking support for camlp5Gravatar letouzey2010-05-19
* After the approval of Bruno, here the patch for the checker.Gravatar soubiran2010-04-29
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
* kills a warning about vo in checker/safe_typingGravatar letouzey2010-03-18
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-23 14:08:07 +0000