aboutsummaryrefslogtreecommitdiffhomepage
path: root/checker/values.ml
Commit message (Expand)AuthorAge
* Simplification: cumulativity information is variance information.Gravatar Gaëtan Gilbert2018-02-10
* Store the conversion oracle in constant and inductive definitions.Gravatar Pierre-Marie Pédrot2018-01-14
* Add interfaces for checker and remove dead code.Gravatar Maxime Dénès2018-01-10
* When declaring constants/inductives use ContextSet if monomorphic.Gravatar Gaëtan Gilbert2017-11-24
* [api] Deprecate all legacy uses of Names in core.Gravatar Emilio Jesus Gallego Arias2017-11-06
* Merge PR #955: Do not hashcons universes beforehandGravatar Maxime Dénès2017-09-15
|\
| * Do not hashcons universes beforehand.Gravatar Pierre-Marie Pédrot2017-09-01
* | Statically enforcing that module types have no retroknowledge.Gravatar Pierre-Marie Pédrot2017-08-29
* | Separating the module_type and module_body types by using a type parameter.Gravatar Pierre-Marie Pédrot2017-08-29
|/
* Removing template polymorphism for definitions.Gravatar Pierre-Marie Pédrot2017-07-26
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
* A short cleanupGravatar Amin Timany2017-06-16
* Clean up universes of constants and inductivesGravatar Amin Timany2017-06-16
* Correct coqchk reductionGravatar Amin Timany2017-06-16
* Fixing the checker.Gravatar Pierre-Marie Pédrot2016-06-18
* Merge PR #79: Let the kernel assume that a (co-)inductive type is positive.Gravatar Pierre-Marie Pédrot2016-06-16
|\
| * Fixing the checker.Gravatar Pierre-Marie Pédrot2016-06-16
* | CLEANUP: Context.{Rel,Named}.Declaration.tGravatar Matej Kosik2016-02-09
* | Update cic.mli MD5 after header update.Gravatar Maxime Dénès2016-01-20
* | Update copyright headers.Gravatar Maxime Dénès2016-01-20
* | Univs: update checkerGravatar Matthieu Sozeau2015-10-02
* | Updating checksum in checker (9c732a5cc continued).Gravatar Hugo Herbelin2015-07-12
* | Option -type-in-type: added support in checker and making it contaminatingGravatar Hugo Herbelin2015-07-10
* | Checker: Fix bug #4282Gravatar Matthieu Sozeau2015-07-07
| * Adjust checker after `Assume [Positive]`.Gravatar Arnaud Spiwack2015-06-25
|/
* Splitting the library representation on disk in two.Gravatar Pierre-Marie Pédrot2015-06-24
* Exporting memory representation of STM tasks for votour.Gravatar Pierre-Marie Pédrot2015-03-25
* Fixing representation of dynamics in votour (again).Gravatar Pierre-Marie Pédrot2015-03-24
* Fix checker after addition of a universe context in with t := c constraints.Gravatar Matthieu Sozeau2015-02-26
* Update hash of cic.mli in checker/values.ml,Gravatar Matthieu Sozeau2015-01-13
* Update headers.Gravatar Maxime Dénès2015-01-12
* Declarations.mli refactoring: module_type_body = module_bodyGravatar Pierre Letouzey2015-01-11
* rename: vi -> vioGravatar Enrico Tassi2015-01-06
* Vi2vo: fix handling of univ constraints coming from the bodyGravatar Enrico Tassi2014-12-23
* Fixing checker representation of values.Gravatar Pierre-Marie Pédrot2014-12-19
* update md5 sums to make "make check" workGravatar Enrico Tassi2014-12-19
* Fixing checker representation of universe lists.Gravatar Pierre-Marie Pédrot2014-12-18
* checker: Change in library on disk values, now using context_sets instead ofGravatar Matthieu Sozeau2014-12-17
* Update checker/values and cic due to changes in case_info and record_body.Gravatar Matthieu Sozeau2014-12-17
* Fix checker/values.ml with latest changes due to projections and universes.Gravatar Matthieu Sozeau2014-09-05
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-25 21:23:48 +0000