aboutsummaryrefslogtreecommitdiffhomepage
path: root/checker/values.ml
Commit message (Expand)AuthorAge
* Completing 5eb53b5bc8d765ed75e965f43f1084e18efc8790 (I unfortunatelyGravatar Hugo Herbelin2014-04-29
* Fixing checker with respect to new kernel name structure and hashmaps.Gravatar Pierre-Marie Pédrot2014-03-18
* vi2vo: universes handling finally fixedGravatar Enrico Tassi2014-03-11
* checker and votour ported to new vo format (after -vi2vo)Gravatar Enrico Tassi2014-02-26
* votour: better error messagesGravatar Enrico Tassi2014-02-26
* fix checker w.r.t. mutual_inductive_body and constant_bodyGravatar Enrico Tassi2014-02-26
* Future: ported to Ephemeron + exception enhancingGravatar gareuselesinge2013-10-18
* Slightly more compact representation of 'a substituted type,Gravatar ppedrot2013-09-14
* Adding dynamic value printing to votour through a registering mechanism.Gravatar ppedrot2013-08-23
* Change in vo format : digest aren't Marshalled anymoreGravatar letouzey2013-08-22
* 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
* Declaremods: major refactoring, stop duplicating libobjects in modulesGravatar letouzey2013-07-17
* 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
* Checker: vo validation is now done in check.ml (and always)Gravatar 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