aboutsummaryrefslogtreecommitdiff
path: root/checker
AgeCommit message (Expand)Author
2012-09-13Made Pp.std_ppcmds opaque.ppedrot
2012-08-08Updating headers.herbelin
2012-06-22Fixing camlp4 compilation w.r.t previous commitppedrot
2012-06-22Added an indirection with respect to Loc in Compat. As many [open Compat]ppedrot
2012-06-02Flushing formatters before program exit.ppedrot
2012-06-01Getting rid of Pp.msgnl and Pp.message.ppedrot
2012-05-30Getting rid of Pp.msgppedrot
2012-05-30More uniformisation in Pp.warn functions.ppedrot
2012-05-29remove many excessive open Util & Errors in mli'sletouzey
2012-04-12lib directory is cut in 2 cma.pboutill
2012-03-26Adapt the checker after commit 15080letouzey
2012-03-26Module names and constant/inductive names are now in two separate namespacesletouzey
2012-03-22Univ: enforce_leq instead of enforce_geq for more uniformityletouzey
2012-03-02Noise for nothingpboutill
2011-11-20Add support for XDG_DATA_HOME and XDG_DATA_DIRS.pboutill
2011-10-26Checker/subtyping.ml: avoid adding in env a module already there (fix #2609)letouzey
2011-10-20More descriptive error messages in checkerglondu
2011-08-08Esubst: make types of substitutions & lifts privatepuech
2011-07-07bug 2423: consider "" as the empty prefixbarras
2011-07-07fixed coqchk usage and man page + added option -coqlibbarras
2011-05-23ported r14149 from v8.3 branch: bug in checker (redefined global)barras
2011-05-17Modops: the strengthening functions can work without any env argumentletouzey
2011-04-14Add directories in COQPATH to search path.herbelin
2011-04-14Reorder search path order, so the standard library is search last.herbelin
2011-04-12Subtyping: align coqtop behavior concerning opaque csts on coqchk's oneletouzey
2011-04-03Lazy loading of opaque proofs: fast as -dont-load-proofs without its drawbacksletouzey
2011-03-04checker: cleanupglondu
2011-03-04checker: add eta-expansionglondu
2011-03-03Propagate recent kernel changes to the checkerletouzey
2011-02-17- Use transparency information all the way through unification andmsozeau
2011-01-31A fine-grain control of inlining at functor application via priority levelsletouzey
2010-12-18Univ.constraints made fully abstract instead of being a Set of abstract stuffletouzey
2010-09-28Fix function applications without labels (OCaml warning 6)glondu
2010-09-24Checker: remove some dead codeletouzey
2010-09-24Some dead code removal, thanks to Oug analyzerletouzey
2010-09-23Fix inconsistency in Prop/Set conversion checkglondu
2010-09-16Explicit Mod_checking signatureglondu
2010-09-15Sharing is not anymore broken by traverse_module.soubiran
2010-09-15Fix likely semantic typosglondu
2010-09-13Fix unescaped end-of-lines (OCaml warning 29)glondu
2010-08-27* checker/Safe_typing.LightenLibrary:regisgia
2010-08-27* (checker|kernel)/Safe_typing:regisgia
2010-08-27* (checker|kernel)/Safe_typing:regisgia
2010-08-27* checker/SafeTyping kernel/SafeTyping:regisgia
2010-08-27* lib/Flags: Replace dont_load_proofs by load_proofs since not loadingregisgia
2010-08-27* Improve documentation of LightenLibrary.regisgia
2010-08-27* (checker|kernel)/Safe_typing: New LightenLibrary.regisgia
2010-07-30adpated the checker to handle coomutative cuts and lazynessbarras
2010-07-24Updated all headers for 8.3 and trunkherbelin
2010-07-22ported bug fix r13290 to checkerbarras
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-02 18:03:39 +0000