aboutsummaryrefslogtreecommitdiff
path: root/checker
AgeCommit message (Expand)Author
2019-02-14[coqlib] Remove `-boot` option for setting the coqlibEmilio Jesus Gallego Arias
2019-02-08Make boot flag into a normal option (no global flag).Gaëtan Gilbert
2019-02-04Primitive integersMaxime Dénès
2019-02-02Merge PR #9250: coqchk: fix check for kelim with functorsPierre-Marie Pédrot
2019-01-21Move inductive_error to Type_errorsGaëtan Gilbert
2019-01-10[checker] avoid some printing in non verbose modeEnrico Tassi
2018-12-19coqchk: fix check for kelim with functorsGaëtan Gilbert
2018-12-12checker: check inductive types by roundtrip through the kernel.Gaëtan Gilbert
2018-12-12Merge PR #8974: Fix mod_subst wrt universe polymorphismMaxime Dénès
2018-12-12Merge PR #9150: [doc] Enable Warning 50 [incorrect doc comment] and fix comme...Maxime Dénès
2018-12-09[doc] Enable Warning 50 [incorrect doc comment] and fix comments.Emilio Jesus Gallego Arias
2018-12-06Revise API for global universes.Gaëtan Gilbert
2018-12-06Fix race condition triggered by fresh universe generationMaxime Dénès
2018-12-05Fix mod_subst wrt universe polymorphismGaëtan Gilbert
2018-11-27Merge PR #8850: Private universes for opaque polymorphic constants.Matthieu Sozeau
2018-11-27Merge PR #8986: Put -indices-matter in typing_flagsMaxime Dénès
2018-11-26Merge PR #9063: [checker] Remove duplicated code from checker / clibPierre-Marie Pédrot
2018-11-26Put -indices-matter in typing_flagsGaëtan Gilbert
2018-11-24[checker] Remove duplicated from checker / clibEmilio Jesus Gallego Arias
2018-11-23Local universes for opaque polymorphic constants.Gaëtan Gilbert
2018-11-23Fix #8937: inductive conversion in coqchk subtypingGaëtan Gilbert
2018-11-21Merge PR #8945: [camlp5] Remove dependency on camlp5.Pierre-Marie Pédrot
2018-11-21[camlp5] Remove dependency on camlp5.Emilio Jesus Gallego Arias
2018-11-21More informative error on vo validation failureGaëtan Gilbert
2018-11-20dune: link kernel in checker instead of copying filesGaëtan Gilbert
2018-11-19Fix dune checker file.Pierre-Marie Pédrot
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 16:35:28 +0000