aboutsummaryrefslogtreecommitdiff
path: root/checker
AgeCommit message (Expand)Author
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
2010-06-02Fix typosglondu
2010-06-01Cleanup: remove code specific for ocaml 3.06letouzey
2010-05-19Add (almost) compatibility with camlp4, without breaking support for camlp5letouzey
2010-04-29After the approval of Bruno, here the patch for the checker.soubiran
2010-04-29Remove the svn-specific $Id$ annotationsletouzey
2010-03-18kills a warning about vo in checker/safe_typingletouzey
2010-03-12fixed confusion between number of cstr arguments and number of pattern variab...barras
2010-02-19added validation of delta_resolver (which seem to have an impact on typing)barras
2010-02-19[checker] fixed vo validation problems, module incompatibilities remainbarras
2010-01-08* Segmenttree: New. A very simple implementation of segment trees.regisgia
2009-12-20* Rewrite [classify_unicode] using standard unicode tables.regisgia
2009-12-01fix coqchk options documentationbarras
2009-10-21This big commit addresses two problems:soubiran
2009-09-17Delete trailing whitespaces in all *.{v,ml*} filesglondu
2009-08-23Fix a small oversight in checker commit 12288.herbelin
2009-08-22Transfers to checker ("let"s in inductive arities + Coq root read-only).herbelin
2009-04-08Some dead code removal + cleanupsletouzey
2009-03-20Many changes in the Makefile infrastructure + a beginning of ocamlbuildletouzey
2009-03-20Directory 'contrib' renamed into 'plugins', to end confusion with archive of ...letouzey
2009-03-02porting r11900 11905 and 11953 to trunkbarras
2009-02-11Report des revisions #11826, #11828 et #11829 de v8.2 vers trunknotin
2009-01-18Backporting from v8.2 to trunk:herbelin
2009-01-06Conversion du fichier 'revision' en un fichier .ml + correction d'un bug dans...notin
2008-12-19Nettoyage des variables Coq et amélioration de coqmktop. Lesnotin
2008-10-15Report des commits 11417 et 11437 de la v8.2soubiran
2008-09-02fixed bug #1927 + univ constraints (module cstrs include cstrs of its subcomp...barras
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-01 10:29:09 +0000