aboutsummaryrefslogtreecommitdiff
path: root/checker/checker.ml
AgeCommit message (Expand)Author
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
2013-02-19Dir_path --> DirPathletouzey
2013-02-18Removing Exc_located and using the new exception enrichementppedrot
2013-02-18use List.rev_map whenever possibleletouzey
2013-02-13make validate repaired via a temporary fix for #2949letouzey
2013-01-28Added backtrace information to anomaliesppedrot
2012-12-14Modulification of dir_pathppedrot
2012-12-14Modulification of identifierppedrot
2012-10-17univ inconsistency error message gives evidence of a cyclebarras
2012-10-06still some more dead code removalletouzey
2012-10-04Getting rid of Compat in the checker.ppedrot
2012-10-04Moved Compat to parsing. This permits to break the dependency of theppedrot
2012-09-17More cleaning on Utils and CList. Some parts of the code beingppedrot
2012-09-13Made Pp.std_ppcmds opaque.ppedrot
2012-08-08Updating headers.herbelin
2012-06-22Fixing camlp4 compilation w.r.t previous commitppedrot
2012-06-22Added an indirection with respect to Loc in Compat. As many [open Compat]ppedrot
2012-06-02Flushing formatters before program exit.ppedrot
2012-06-01Getting rid of Pp.msgnl and Pp.message.ppedrot
2012-05-30More uniformisation in Pp.warn functions.ppedrot
2012-04-12lib directory is cut in 2 cma.pboutill
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 14:34:24 +0000