aboutsummaryrefslogtreecommitdiffhomepage
path: root/checker
Commit message (Expand)AuthorAge
* More monomorphic List.mem + List.assoc + ...Gravatar letouzey2013-10-24
* inductive.ml : get rid of some obvious (Lazy.force (lazy t))Gravatar letouzey2013-10-24
* Rtree : cleanup of the comparing codeGravatar letouzey2013-10-24
* Get rid of polymorphic equality in "checker/subtyping.ml".Gravatar xclerc2013-10-24
* Turn many List.assoc into List.assoc_fGravatar letouzey2013-10-24
* cList.index is now cList.index_f, same for index0Gravatar letouzey2013-10-23
* Future: ported to Ephemeron + exception enhancingGravatar gareuselesinge2013-10-18
* Ephemeron: marshaling friendly keysGravatar gareuselesinge2013-10-18
* Getting rid of the use of deprecated elements (from the OCaml standard library).Gravatar xclerc2013-10-14
* Slightly more compact representation of 'a substituted type,Gravatar ppedrot2013-09-14
* Moving Searchstack to CStack, and normalizing names a bit.Gravatar ppedrot2013-09-06
* Added a more efficient way to recover the domain of a map.Gravatar ppedrot2013-08-25
* Adding dynamic value printing to votour through a registering mechanism.Gravatar ppedrot2013-08-23
* Misc changes around coqtop.ml :Gravatar letouzey2013-08-22
* Change in vo format : digest aren't Marshalled anymoreGravatar letouzey2013-08-22
* Fixing votourGravatar ppedrot2013-08-20
* Fix compilation of coqcheckGravatar gareuselesinge2013-08-20
* Declarations.mli: reorganization of modular structuresGravatar letouzey2013-08-20
* Repair coqcheck : constant_body constraints are also futureGravatar letouzey2013-08-20
* checker validation fixed w.r.t. FuturesGravatar gareuselesinge2013-08-09
* checker validation made a bit more verboseGravatar gareuselesinge2013-08-09
* State Transaction MachineGravatar gareuselesinge2013-08-08
* Declaremods: major refactoring, stop duplicating libobjects in modulesGravatar letouzey2013-07-17
* Added a generic notion of hook. Hooks are functions to be setGravatar ppedrot2013-05-12
* Uniformizing the [if_warn] flag used for warning printing and putGravatar ppedrot2013-05-08
* Remove deprecated option -no-hash-consing (currently doing nothing)Gravatar letouzey2013-04-23
* Checker: vo validation checks the absence of Var/Evar/MetaGravatar letouzey2013-04-15
* Checker : a md5-based way to ensure checker/values.ml is always in syncGravatar letouzey2013-04-15
* votour: a small tool for guided tours of .voGravatar letouzey2013-04-15
* Checker: vo validation is now done in check.ml (and always)Gravatar letouzey2013-04-15
* Checker: get rid of code handling section variablesGravatar letouzey2013-04-15
* Checker: empty sections hardcoded in cb and mindGravatar letouzey2013-04-15
* Checker: reified encoding of .vo types in values.mlGravatar letouzey2013-04-15
* Checker: regroup all vo-related types in cic.mliGravatar letouzey2013-04-15
* Revised infrastructure for lazy loading of opaque proofsGravatar letouzey2013-04-02
* Mod_subst.force: avoid using join when only one substGravatar letouzey2013-04-02
* Minor cleanup concerning Mod_subst.MBImapGravatar letouzey2013-04-02
* Safe_typing+Libary: use some arrays instead of lists in vo structuresGravatar letouzey2013-03-28
* Minor code cleaning in CArray / CList.Gravatar ppedrot2013-03-23
* Removing mandatory suffixes for library files.Gravatar ppedrot2013-03-21
* Checker: simplify a bit its exception handlerGravatar letouzey2013-03-17
* Fix compilation of coqchk (broken by commit 16268), bis repetitaGravatar letouzey2013-03-13
* Fix compilation of coqchk (broken by commit 16268)Gravatar letouzey2013-03-13
* Restrict (try...with...) to avoid catching critical exn (part 2)Gravatar letouzey2013-03-12
* Restrict (try...with...) to avoid catching critical exn (part 1)Gravatar letouzey2013-03-12
* More monomorphization.Gravatar ppedrot2013-03-05
* Names: shortcuts for building {kn, constant, mind} with empty sectionsGravatar letouzey2013-02-26
* Names: Modularize constant and mutual_inductiveGravatar letouzey2013-02-26
* Dir_path --> DirPathGravatar letouzey2013-02-19
* Names: revised representation of constants and mutual_inductiveGravatar letouzey2013-02-19