aboutsummaryrefslogtreecommitdiff
path: root/checker
AgeCommit message (Expand)Author
2019-03-14Repair relevance marks in-kernel.Gaëtan Gilbert
2019-03-14Add relevance marks on binders.Gaëtan Gilbert
2019-03-14Add a non-cumulative impredicative universe SProp.Gaëtan Gilbert
2019-03-14Merge PR #9700: [dune] [checker] Don't install internal checker library.Théo Zimmermann
2019-03-11Nicer error for bad primitive types (through type_errors etc)Gaëtan Gilbert
2019-03-05[dune] [checker] Don't install internal checker library.Emilio Jesus Gallego Arias
2019-02-28Constructor type information uses the expanded form.Pierre-Marie Pédrot
2019-02-25Merge PR #9511: Enable whitespace checking for some forgotten files.Théo Zimmermann
2019-02-22[library] Remove `-boot` option.Emilio Jesus Gallego Arias
2019-02-21Fix #9613 use -coqlib when invoking coqchkGaëtan Gilbert
2019-02-20Enable whitespace checking for some forgotten files.Gaëtan Gilbert
2019-02-20Merge PR #9560: [coqlib] Remove `-boot` option for setting the coqlibEnrico Tassi
2019-02-17Separate variance and universe fields in inductives.Gaëtan Gilbert
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 13:01:15 +0000