aboutsummaryrefslogtreecommitdiff
path: root/checker
AgeCommit message (Expand)Author
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
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-25 01:20:51 +0000