aboutsummaryrefslogtreecommitdiff
path: root/checker
AgeCommit message (Expand)Author
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-06Bring back context printing in checkerMaxime Dénès
2018-11-06Checker now disables VM and nativeMaxime Dénès
2018-11-06[checker] Check univ constraints induced by module subtypingMaxime Dénès
2018-11-06[checker] Fix "error related to inductive types"Maxime Dénès
2018-11-06[checker] Refactor by sharing code with the kernelMaxime Dénès
2018-11-05Merge PR #8870: Pass native and VM flags to the kernel through environmentPierre-Marie Pédrot
2018-11-05Merge PR #8874: Fix #8873: coqchk on inductive with letin parameterPierre-Marie Pédrot
2018-11-05Merge PR #8882: Fix #8881: validate fails to use inductive equivalence in cas...Pierre-Marie Pédrot
2018-11-05Pass native and VM flags to the kernel through environmentMaxime Dénès
2018-10-31Fix #8881: validate fails to use inductive equivalence in case_infoGaëtan Gilbert
2018-10-31Fix #8876: expected number of arguments for cumulative constructorsGaëtan Gilbert
2018-10-31Fix #8873: coqchk on inductive with letin parameterGaëtan Gilbert
2018-10-29Rename checker/{main->coqchk}Gaëtan Gilbert
2018-10-26Merge PR #8753: [build] Refactoring of config lib and ocamldebug tweaks.Gaëtan Gilbert
2018-10-26Merge PR #8707: Separate cache representation between CClosure and CBVMaxime Dénès
2018-10-23[build] Refactoring to config lib and ocamldebug tweaks.Emilio Jesus Gallego Arias
2018-10-22Merge PR #8708: Stupid but critical unfolding heuristic.Maxime Dénès
2018-10-11Also clean up the checker w.r.t. unused closure data.Pierre-Marie Pédrot
2018-10-11Stupid but critical unfolding heuristic.Pierre-Marie Pédrot
2018-10-09[coqchk] Fix checking of records in module signaturesVincent Laporte
2018-10-09[coqchk] Fix checking of inductive typesVincent Laporte
2018-10-09[coqchk] Fix case_info for primitive recordsVincent Laporte
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-27 23:00:34 +0000