aboutsummaryrefslogtreecommitdiff
path: root/checker/values.ml
AgeCommit message (Expand)Author
2018-11-23Local universes for opaque polymorphic constants.Gaëtan Gilbert
2018-11-21More informative error on vo validation failureGaëtan Gilbert
2018-11-09Use arrays of names instead of lists in abstract universe names.Pierre-Marie Pédrot
2018-11-09Actually store the bound name information in the abstract universe context.Pierre-Marie Pédrot
2018-11-05Pass native and VM flags to the kernel through environmentMaxime Dénès
2018-10-05[kernel] Remove section paths from `KerName.t`Maxime Dénès
2018-09-26Merge PR #8102: Fix #8043: Unsafe assignment in checker.Maxime Dénès
2018-09-07Canonical representation of kernel substitutions.Pierre-Marie Pédrot
2018-07-26Turn the kernel reduction sharing flag into an argument passed in the cache.Pierre-Marie Pédrot
2018-07-24Projections use index representationGaëtan Gilbert
2018-07-20Fix #8043: Unsafe assignment in checker.Pierre-Marie Pédrot
2018-06-26Remove Sorts.contentsGaëtan Gilbert
2018-06-23Using more general information for primitive records.Pierre-Marie Pédrot
2018-06-23Change the proj_ind field from MutInd.t to inductive.Pierre-Marie Pédrot
2018-06-19Merge PR #7841: Remove CanaryPierre-Marie Pédrot
2018-06-18Remove Canary.whitequark
2018-06-17Remove the proj_body field from the kernel.Pierre-Marie Pédrot
2018-06-17Remove the proj_eta field of the kernel.Pierre-Marie Pédrot
2018-06-17Getting rid of the const_proj field in the kernel.Pierre-Marie Pédrot
2018-06-07Fix the checker by merely adapting the data structure.Pierre-Marie Pédrot
2018-05-31Reduce circular dependency constants <-> projectionsGaëtan Gilbert
2018-03-28[api] Deprecate a couple of aliases that we missed.Emilio Jesus Gallego Arias
2018-02-27Update headers following #6543.Théo Zimmermann
2018-02-16Extrude monomorphic universe contexts from with Definition constraints.Pierre-Marie Pédrot
2018-02-10Simplification: cumulativity information is variance information.Gaëtan Gilbert
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 18:02:02 +0000