aboutsummaryrefslogtreecommitdiff
path: root/checker
AgeCommit message (Expand)Author
2014-01-19Fixing checker compilation, which was broken by the following commit:Pierre-Marie Pédrot
2014-01-18Relaxing the sort elimination check to allow for let-bindings in arities.Maxime Dénès
2014-01-15Christmas is over...Maxime Dénès
2014-01-04.vi files: .vo files without proofsEnrico Tassi
2013-10-24More monomorphic List.mem + List.assoc + ...letouzey
2013-10-24inductive.ml : get rid of some obvious (Lazy.force (lazy t))letouzey
2013-10-24Rtree : cleanup of the comparing codeletouzey
2013-10-24Get rid of polymorphic equality in "checker/subtyping.ml".xclerc
2013-10-24Turn many List.assoc into List.assoc_fletouzey
2013-10-23cList.index is now cList.index_f, same for index0letouzey
2013-10-18Future: ported to Ephemeron + exception enhancinggareuselesinge
2013-10-18Ephemeron: marshaling friendly keysgareuselesinge
2013-10-14Getting rid of the use of deprecated elements (from the OCaml standard library).xclerc
2013-09-14Slightly more compact representation of 'a substituted type,ppedrot
2013-09-06Moving Searchstack to CStack, and normalizing names a bit.ppedrot
2013-08-25Added a more efficient way to recover the domain of a map.ppedrot
2013-08-23Adding dynamic value printing to votour through a registering mechanism.ppedrot
2013-08-22Misc changes around coqtop.ml :letouzey
2013-08-22Change in vo format : digest aren't Marshalled anymoreletouzey
2013-08-20Fixing votourppedrot
2013-08-20Fix compilation of coqcheckgareuselesinge
2013-08-20Declarations.mli: reorganization of modular structuresletouzey
2013-08-20Repair coqcheck : constant_body constraints are also futureletouzey
2013-08-09checker validation fixed w.r.t. Futuresgareuselesinge
2013-08-09checker validation made a bit more verbosegareuselesinge
2013-08-08State Transaction Machinegareuselesinge
2013-07-17Declaremods: major refactoring, stop duplicating libobjects in modulesletouzey
2013-05-12Added a generic notion of hook. Hooks are functions to be setppedrot
2013-05-08Uniformizing the [if_warn] flag used for warning printing and putppedrot
2013-04-23Remove deprecated option -no-hash-consing (currently doing nothing)letouzey
2013-04-15Checker: vo validation checks the absence of Var/Evar/Metaletouzey
2013-04-15Checker : a md5-based way to ensure checker/values.ml is always in syncletouzey
2013-04-15votour: a small tool for guided tours of .voletouzey
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-06 16:48:33 +0000