aboutsummaryrefslogtreecommitdiff
path: root/checker/values.ml
AgeCommit message (Expand)Author
2018-01-14Store the conversion oracle in constant and inductive definitions.Pierre-Marie Pédrot
2018-01-10Add interfaces for checker and remove dead code.Maxime Dénès
2017-11-24When declaring constants/inductives use ContextSet if monomorphic.Gaëtan Gilbert
2017-11-06[api] Deprecate all legacy uses of Names in core.Emilio Jesus Gallego Arias
2017-09-15Merge PR #955: Do not hashcons universes beforehandMaxime Dénès
2017-09-01Do not hashcons universes beforehand.Pierre-Marie Pédrot
2017-08-29Statically enforcing that module types have no retroknowledge.Pierre-Marie Pédrot
2017-08-29Separating the module_type and module_body types by using a type parameter.Pierre-Marie Pédrot
2017-07-26Removing template polymorphism for definitions.Pierre-Marie Pédrot
2017-07-04Bump year in headers.Pierre-Marie Pédrot
2017-06-16A short cleanupAmin Timany
2017-06-16Clean up universes of constants and inductivesAmin Timany
2017-06-16Correct coqchk reductionAmin Timany
2016-06-18Fixing the checker.Pierre-Marie Pédrot
2016-06-16Merge PR #79: Let the kernel assume that a (co-)inductive type is positive.Pierre-Marie Pédrot
2016-06-16Fixing the checker.Pierre-Marie Pédrot
2016-02-09CLEANUP: Context.{Rel,Named}.Declaration.tMatej Kosik
2016-01-20Update cic.mli MD5 after header update.Maxime Dénès
2016-01-20Update copyright headers.Maxime Dénès
2015-10-02Univs: update checkerMatthieu Sozeau
2015-07-12Updating checksum in checker (9c732a5cc continued).Hugo Herbelin
2015-07-10Option -type-in-type: added support in checker and making it contaminatingHugo Herbelin
2015-07-07Checker: Fix bug #4282Matthieu Sozeau
2015-06-25Adjust checker after `Assume [Positive]`.Arnaud Spiwack
2015-06-24Splitting the library representation on disk in two.Pierre-Marie Pédrot
2015-03-25Exporting memory representation of STM tasks for votour.Pierre-Marie Pédrot
2015-03-24Fixing representation of dynamics in votour (again).Pierre-Marie Pédrot
2015-02-26Fix checker after addition of a universe context in with t := c constraints.Matthieu Sozeau
2015-01-13Update hash of cic.mli in checker/values.ml,Matthieu Sozeau
2015-01-12Update headers.Maxime Dénès
2015-01-11Declarations.mli refactoring: module_type_body = module_bodyPierre Letouzey
2015-01-06rename: vi -> vioEnrico Tassi
2014-12-23Vi2vo: fix handling of univ constraints coming from the bodyEnrico Tassi
2014-12-19Fixing checker representation of values.Pierre-Marie Pédrot
2014-12-19update md5 sums to make "make check" workEnrico Tassi
2014-12-18Fixing checker representation of universe lists.Pierre-Marie Pédrot
2014-12-17checker: Change in library on disk values, now using context_sets instead ofMatthieu Sozeau
2014-12-17Update checker/values and cic due to changes in case_info and record_body.Matthieu Sozeau
2014-09-05Fix checker/values.ml with latest changes due to projections and universes.Matthieu Sozeau
2014-04-29Completing 5eb53b5bc8d765ed75e965f43f1084e18efc8790 (I unfortunatelyHugo Herbelin
2014-03-18Fixing checker with respect to new kernel name structure and hashmaps.Pierre-Marie Pédrot
2014-03-11vi2vo: universes handling finally fixedEnrico Tassi
2014-02-26checker and votour ported to new vo format (after -vi2vo)Enrico Tassi
2014-02-26votour: better error messagesEnrico Tassi
2014-02-26fix checker w.r.t. mutual_inductive_body and constant_bodyEnrico Tassi
2013-10-18Future: ported to Ephemeron + exception enhancinggareuselesinge
2013-09-14Slightly more compact representation of 'a substituted type,ppedrot
2013-08-23Adding dynamic value printing to votour through a registering mechanism.ppedrot
2013-08-22Change in vo format : digest aren't Marshalled anymoreletouzey
2013-08-20Declarations.mli: reorganization of modular structuresletouzey
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 13:32:38 +0000