aboutsummaryrefslogtreecommitdiff
path: root/checker/checker.ml
AgeCommit message (Expand)Author
2021-03-03[build] Split stdlib to it's own opam package.Emilio Jesus Gallego Arias
2021-02-25Merge PR #13202: Infrastructure for fine-grained debug flagscoqbot-app[bot]
2021-02-24Infrastructure for fine-grained debug flagsMaxime Dénès
2021-02-16Get rid of the compilation date from the binaries to make them more stable.Guillaume Melquiond
2021-01-06Further pushing up the printing and sorting of universes.Pierre-Marie Pédrot
2020-11-16Infrastructure for cumulative inductive syntax (no grammar extension yet)Gaëtan Gilbert
2020-07-05Merge PR #12613: Remove deprecated (in 8.8 #6277) coqchk -IPierre-Marie Pédrot
2020-07-01UIP in SPropGaëtan Gilbert
2020-07-01Remove deprecated (in 8.8 #6277) coqchk -IGaëtan Gilbert
2020-05-22[coqchk] Fix #5030Pierre Roux
2020-03-18Update headers in the whole code base.Théo Zimmermann
2019-11-21[coq] Untabify the whole ML codebase.Emilio Jesus Gallego Arias
2019-06-17Update ml-style headers to new year.Théo Zimmermann
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-11Nicer error for bad primitive types (through type_errors etc)Gaëtan Gilbert
2019-02-22[library] Remove `-boot` option.Emilio Jesus Gallego Arias
2019-02-21Fix #9613 use -coqlib when invoking coqchkGaë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-01-21Move inductive_error to Type_errorsGaëtan Gilbert
2018-12-12checker: check inductive types by roundtrip through the kernel.Gaëtan Gilbert
2018-11-26Put -indices-matter in typing_flagsGaëtan Gilbert
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] Refactor by sharing code with the kernelMaxime Dénès
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-03-07[checker] Printer cleanup.Emilio Jesus Gallego Arias
2018-02-27Update headers following #6543.Théo Zimmermann
2018-02-09[error] Replace msg_error by a proper exception.Emilio Jesus Gallego Arias
2018-01-24fix space in coqchk errorRalf Jung
2017-12-01Documenting the -Q flag of coqchk.Pierre-Marie Pédrot
2017-11-29Mark the -I option in coqchk as deprecated and merge it with -Q.Pierre-Marie Pédrot
2017-11-29Add a -Q option to coqchck.Pierre-Marie Pédrot
2017-11-29Allow to pass physical files to coqchk.Pierre-Marie Pédrot
2017-11-06[feedback] Helper to print feedback messages in the console.Emilio Jesus Gallego Arias
2017-09-25Merge PR #1075: Re-enable checker error messagesMaxime Dénès
2017-09-21Adapt checker to change in locations.Maxime Dénès
2017-09-21[checker] Add missing Feedback printer (BZ#5587)Emilio Jesus Gallego Arias
2017-09-20[flags] Flag `open Flags`Emilio Jesus Gallego Arias
2017-07-04Bump year in headers.Pierre-Marie Pédrot
2017-05-27[cleanup] Unify all calls to the error function.Emilio Jesus Gallego Arias
2017-04-27Remove uses of [Flags.make_silent]Gaetan Gilbert
2017-04-27Remove unused [rec] keywordsGaetan Gilbert
2016-10-02Merge branch 'v8.6'Pierre-Marie Pédrot
2016-09-30Merge remote-tracking branch 'github/pr/257' into v8.6Maxime Dénès
2016-09-29fix bug 3683 : adds references to the web site for the bug trackerYves Bertot
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 09:41:49 +0000