aboutsummaryrefslogtreecommitdiff
path: root/checker/checker.ml
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-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
2016-08-19Make the user_err header an optional parameter.Emilio Jesus Gallego Arias
2016-08-18[checker] Fix/fine tune printing.Emilio Jesus Gallego Arias
2016-07-03errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...Pierre Letouzey
2016-06-18Fixing the checker.Pierre-Marie Pédrot
2016-06-09Merge branch 'v8.5'Pierre-Marie Pédrot
2016-06-07Do not use COQLIBS for the validate rule produced by coq_makefile (bug #4693).Guillaume Melquiond
2016-05-31Feedback cleanupEmilio Jesus Gallego Arias
2016-01-21Merge branch 'v8.5'Pierre-Marie Pédrot
2016-01-20Update copyright headers.Maxime Dénès
2016-01-06Remove deprecated command-line options such as "-as".Guillaume Melquiond
2015-12-31Remove unused function Checker.print_loc.Guillaume Melquiond
2015-07-10Option -type-in-type: added support in checker and making it contaminatingHugo Herbelin
2015-04-23Remove almost all the uses of string concatenation when building error messages.Guillaume Melquiond
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 13:18:31 +0000