aboutsummaryrefslogtreecommitdiff
path: root/checker
AgeCommit message (Expand)Author
2018-10-09[coqchk] Fix subterm relation for primitive projectionsVincent Laporte
2018-10-09[coqchk] Fix guard condition with commutative cutsVincent Laporte
2018-10-05[kernel] Remove section paths from `KerName.t`Maxime Dénès
2018-10-03[dune] Add `(package coq)` scope to artifacts.Emilio Jesus Gallego Arias
2018-10-03Merge PR #8563: Fix checker soundness bug with polymorphism capturing global ...Pierre-Marie Pédrot
2018-10-01Fix checker soundness bug with polymorphism capturing global univsGaëtan Gilbert
2018-10-01[lib] [flags] Move coqlib handling out of `Flags`Emilio Jesus Gallego Arias
2018-09-28[dune] Pack checker to avoid [odoc] problems + build doc for plugins.Emilio Jesus Gallego Arias
2018-09-26Fix votour compilation after #8102.Pierre-Marie Pédrot
2018-09-26Merge PR #8102: Fix #8043: Unsafe assignment in checker.Maxime Dénès
2018-09-23Checking if low-level name printers are used on purpose or not.Hugo Herbelin
2018-09-07Canonical representation of kernel substitutions.Pierre-Marie Pédrot
2018-09-05[build] Preliminary support for building Coq with `dune`.Emilio Jesus Gallego Arias
2018-07-26Turn the kernel reduction sharing flag into an argument passed in the cache.Pierre-Marie Pédrot
2018-07-24Fix #7329: coqchk Include with primitive projectionsGaëtan Gilbert
2018-07-24Projections use index representationGaëtan Gilbert
2018-07-20Fix #8043: Unsafe assignment in checker.Pierre-Marie Pédrot
2018-07-03checker Indtypes: remove unused argumentsGaëtan Gilbert
2018-07-03checker Modops strengthening: remove unused argument resolverGaëtan Gilbert
2018-07-03Subtyping.check_constant: remove unused module path argument.Gaëtan Gilbert
2018-07-03Inductive.extract_stack,filter_stack_domain: remove unused argumentsGaëtan Gilbert
2018-06-26Remove Sorts.contentsGaëtan Gilbert
2018-06-25Merge PR #7798: Remove hack skipping comparison of algebraic universes in sub...Matthieu Sozeau
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-22Remove hack skipping comparison of algebraic universes in subtyping.Gaëtan Gilbert
2018-06-21Remove enforce_leq from checkerGaëtan Gilbert
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-06-04Merge PR #7552: Fix #7539: Checker does not properly handle negative coinduct...Matthieu Sozeau
2018-05-31Reduce circular dependency constants <-> projectionsGaëtan Gilbert
2018-05-25Merge PR #7325: Fix #7323: coqchk puts polymorphic univs of inductive in glob...Pierre-Marie Pédrot
2018-05-24Merge PR #7177: Unifying names of "smart" combinators + adding combinators in...Pierre-Marie Pédrot
2018-05-24Fix #7323: coqchk puts polymorphic univs of inductive in global envGaëtan Gilbert
2018-05-24Merge PR #7328: Fix #7327: coqchk subtyping of polymorphic constantsPierre-Marie Pédrot
2018-05-24Merge PR #7317: Fix #6798: coqchk ignores ugraph when comparing constant inst...Pierre-Marie Pédrot
2018-05-23Moving Rtree.smart_map into Rtree.Smart.map.Hugo Herbelin
2018-05-23Moving Option.smart_map to Option.Smart.map.Hugo Herbelin
2018-05-23Collecting List.smart_* functions into a module List.Smart.Hugo Herbelin
2018-05-23Collecting Array.smart_* functions into a module Array.Smart.Hugo Herbelin
2018-05-18Fix #7539: Checker does not properly handle negative coinductive types.Pierre-Marie Pédrot
2018-05-13Infrastructure for ocamldebug on the checkerGaëtan Gilbert
2018-04-23Fix #7327: coqchk subtyping of polymorphic constantsGaëtan Gilbert
2018-04-20Fix #6798: coqchk ignores ugraph when comparing constant instancesGaëtan Gilbert
2018-03-28[api] Deprecate a couple of aliases that we missed.Emilio Jesus Gallego Arias
2018-03-09Merge PR #6800: [checker] Printer cleanup.Maxime Dénès
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 21:27:36 +0000