aboutsummaryrefslogtreecommitdiff
path: root/checker/checker.ml
AgeCommit message (Expand)Author
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
2012-03-02Noise for nothingpboutill
2011-11-20Add support for XDG_DATA_HOME and XDG_DATA_DIRS.pboutill
2011-07-07bug 2423: consider "" as the empty prefixbarras
2011-07-07fixed coqchk usage and man page + added option -coqlibbarras
2011-04-14Add directories in COQPATH to search path.herbelin
2011-04-14Reorder search path order, so the standard library is search last.herbelin
2010-09-28Fix function applications without labels (OCaml warning 6)glondu
2010-09-24Checker: remove some dead codeletouzey
2010-09-13Fix unescaped end-of-lines (OCaml warning 29)glondu
2010-07-24Updated all headers for 8.3 and trunkherbelin
2010-06-01Cleanup: remove code specific for ocaml 3.06letouzey
2010-05-19Add (almost) compatibility with camlp4, without breaking support for camlp5letouzey
2010-04-29Remove the svn-specific $Id$ annotationsletouzey
2010-02-19[checker] fixed vo validation problems, module incompatibilities remainbarras
2009-12-01fix coqchk options documentationbarras
2009-09-17Delete trailing whitespaces in all *.{v,ml*} filesglondu
2009-08-22Transfers to checker ("let"s in inductive arities + Coq root read-only).herbelin
2009-03-20Directory 'contrib' renamed into 'plugins', to end confusion with archive of ...letouzey
2009-03-02porting r11900 11905 and 11953 to trunkbarras
2009-02-11Report des revisions #11826, #11828 et #11829 de v8.2 vers trunknotin
2009-01-06Conversion du fichier 'revision' en un fichier .ml + correction d'un bug dans...notin
2008-12-19Nettoyage des variables Coq et amélioration de coqmktop. Lesnotin