aboutsummaryrefslogtreecommitdiff
path: root/toplevel/cerrors.ml
AgeCommit message (Expand)Author
2014-05-06This commit adds full universe polymorphism and fast projections to Coq.Matthieu Sozeau
2014-04-23Removing dead code, thanks to new OCaml warnings and a bit of scripting.Pierre-Marie Pédrot
2014-03-05Remove some dead-code (thanks to ocaml warnings)Pierre Letouzey
2014-01-30Fixing backtrace handling here and there.Pierre-Marie Pédrot
2013-12-09Fix printing of Ltac's backtrace.Arnaud Spiwack
2013-11-02Replaced monads.ml by an essentially equivalent proofview_gen.ml generated by...aspiwack
2013-05-30Removing a useless location in ltac trace mechanism.ppedrot
2013-05-28Getting rid of LtacLocated exception transformer.ppedrot
2013-03-14Embedded exns in LtacLocated and EvaluatedError satisfy Errors.noncriticalletouzey
2013-03-14Cerrors: get rid of some FIXMEletouzey
2013-02-18Removing Exc_located and using the new exception enrichementppedrot
2013-02-17Revised the Ltac trace mechanism so that trace breaking due toherbelin
2012-12-04Removed Compat.Exc_located outside of compat.ml4, as a consequence ofherbelin
2012-11-26Removed some FIXME related to equality on universes.ppedrot
2012-11-26Monomorphization (toplevel)ppedrot
2012-10-17univ inconsistency error message gives evidence of a cyclebarras
2012-10-04Moved Compat to parsing. This permits to break the dependency of theppedrot
2012-10-02Remove some more "open" and dead code thanks to OCaml4 warningsletouzey
2012-09-14Partial revert of Yann commit in order to use CLib.List when openingppedrot
2012-09-14This patch removes unused "open" (automatically generated fromregisgia
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-03-02Noise for nothingpboutill
2011-05-17More work on error handlingletouzey
2011-05-16Repair the "Fail" command after recent changes in exception handlingletouzey
2011-05-15Turning Sys_error into error by default instead of anomaly. After all,herbelin
2011-05-13A new mechanism to handle errors.aspiwack
2011-03-16Finish branching functions handling module errors (cf. r13886)letouzey
2010-11-16Remove redundant clause (and fix compatibility issue)glondu
2010-11-07Delayed the evar normalization in error messages to the last minuteherbelin
2010-11-07correcting a non catch error reported as an anomaly (Ploc.Exc)jforest
2010-10-26Compatibility camlp4/camlp5herbelin
2010-10-23Fixing bug #2412, continued (preprocessing of Ltac Debug errorsherbelin
2010-10-23Fixing bug #2412 (preprocessing of Ltac Debug errors forgotten in r13431).herbelin
2010-09-18Fixing bugs #2347 (part 2) and #2388: error message printing was doneherbelin
2010-08-26Fix an error message ot having the ERror: prefix.courtieu
2010-07-24Updated all headers for 8.3 and trunkherbelin
2010-06-01Cleanup: remove code specific for ocaml 3.06letouzey
2010-06-01restore handling of lexer errorsletouzey
2010-05-19Add (almost) compatibility with camlp4, without breaking support for camlp5letouzey
2010-04-30Fail: a way to check that a command is refused without blocking a scriptletouzey
2010-04-29Remove the svn-specific $Id$ annotationsletouzey
2010-04-27Added a new exception for already declared Schemes, vsiles
2009-10-04Removal of trailing spaces.serpyc
2009-09-26Fixed a hole in glob_tactic that allowed some Ltac code to refer toherbelin
2009-09-17Delete trailing whitespaces in all *.{v,ml*} filesglondu
2009-06-11Use a lazy value for the message in FailError, so that it won't bemsozeau
2009-03-04Timeout message was not always displayedbarras
2008-08-05Correction de bugs:herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-20 08:26:44 +0000