aboutsummaryrefslogtreecommitdiff
path: root/checker
AgeCommit message (Expand)Author
2013-04-15Checker: vo validation is now done in check.ml (and always)letouzey
2013-04-15Checker: get rid of code handling section variablesletouzey
2013-04-15Checker: empty sections hardcoded in cb and mindletouzey
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
2013-04-02Mod_subst.force: avoid using join when only one substletouzey
2013-04-02Minor cleanup concerning Mod_subst.MBImapletouzey
2013-03-28Safe_typing+Libary: use some arrays instead of lists in vo structuresletouzey
2013-03-23Minor code cleaning in CArray / CList.ppedrot
2013-03-21Removing mandatory suffixes for library files.ppedrot
2013-03-17Checker: simplify a bit its exception handlerletouzey
2013-03-13Fix compilation of coqchk (broken by commit 16268), bis repetitaletouzey
2013-03-13Fix compilation of coqchk (broken by commit 16268)letouzey
2013-03-12Restrict (try...with...) to avoid catching critical exn (part 2)letouzey
2013-03-12Restrict (try...with...) to avoid catching critical exn (part 1)letouzey
2013-03-05More monomorphization.ppedrot
2013-02-26Names: shortcuts for building {kn, constant, mind} with empty sectionsletouzey
2013-02-26Names: Modularize constant and mutual_inductiveletouzey
2013-02-19Dir_path --> DirPathletouzey
2013-02-19Names: revised representation of constants and mutual_inductiveletouzey
2013-02-18Removing Exc_located and using the new exception enrichementppedrot
2013-02-18Added exception enrichment. Now one can define additional arbitraryppedrot
2013-02-18use List.rev_map whenever possibleletouzey
2013-02-18Minor code cleanups, especially take advantage of Dir_path.is_emptyletouzey
2013-02-13make validate repaired via a temporary fix for #2949letouzey
2013-02-12Checker: re-sync vo structures after Maxime's commit 16136letouzey
2013-02-03Fixing coqchk compilation after commit r16183ppedrot
2013-01-28Added backtrace primitives.ppedrot
2013-01-28Uniformization of the "anomaly" command.ppedrot
2013-01-28Added backtrace information to anomaliesppedrot
2012-12-19Array.create is deprecatedpboutill
2012-12-18Modulification of mod_bound_idppedrot
2012-12-18Modulification of Labelppedrot
2012-12-14Modulification of dir_pathppedrot
2012-12-14Modulification of identifierppedrot
2012-12-14Moving hcons_string to String namespace.ppedrot
2012-11-20Cleaning and small optimization in CList.ppedrot
2012-11-13Added a CString module.ppedrot
2012-11-08Added an Int module with dummy utility functions.ppedrot
2012-10-17univ inconsistency error message gives evidence of a cyclebarras
2012-10-06still some more dead code removalletouzey
2012-10-04Getting rid of Compat in the checker.ppedrot
2012-10-04Moved Compat to parsing. This permits to break the dependency of theppedrot
2012-09-26Reusing the Hashset data structure in Hashcons. Hopefully, this shouldppedrot
2012-09-18More cleanup of Util: utf8 aspects moved to a new file unicode.mlletouzey
2012-09-18Cleaning interface of Util.ppedrot
2012-09-17More cleaning on Utils and CList. Some parts of the code beingppedrot
2012-09-14As r15801: putting everything from Util.array_* to CArray.*.ppedrot
2012-09-14Moving Utils.list_* to a proper CList module, which includes stdlibppedrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-02 14:51:19 +0000