aboutsummaryrefslogtreecommitdiff
path: root/checker/checker.ml
AgeCommit message (Expand)Author
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
2015-03-31Removing references to deprecated syntax -I/-R -as.Pierre-Marie Pédrot
2015-02-12Revert "Using same code for browsing physical directories in coqtop and coqdep."Hugo Herbelin
2015-02-12Revert "Capital letter in plugins." (Sorry, was not intended to be pushed)Hugo Herbelin
2015-02-12Capital letter in plugins.Hugo Herbelin
2015-02-12Using same code for browsing physical directories in coqtop and coqdep.Hugo Herbelin
2015-01-12Update headers.Maxime Dénès
2014-11-14Exit with code 129 when an anomaly occurs.Xavier Clerc
2014-06-10Removing explanations of universe inconsistencies from the checker. TheyPierre-Marie Pédrot
2014-05-08Adapt the checker to polymorphic universes and projections (untested).Matthieu Sozeau
2014-04-08printer for coqchkEnrico Tassi
2014-03-18Printing backtraces in coqchk while in debug mode.Pierre-Marie Pédrot
2014-02-26checker: less useless error messagesEnrico Tassi
2013-08-22Misc changes around coqtop.ml :letouzey
2013-04-23Remove deprecated option -no-hash-consing (currently doing nothing)letouzey
2013-04-15Checker: regroup all vo-related types in cic.mliletouzey
2013-03-17Checker: simplify a bit its exception handlerletouzey
2013-03-12Restrict (try...with...) to avoid catching critical exn (part 1)letouzey
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-13 07:59:13 +0000