aboutsummaryrefslogtreecommitdiff
path: root/toplevel/cerrors.ml
AgeCommit message (Expand)Author
2016-07-03rename toplevel/cerror.ml into explainErr.ml (too close to the new lib/cError...Pierre Letouzey
2016-07-03errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...Pierre Letouzey
2016-06-29A new infrastructure for warnings.Maxime Dénès
2016-05-09Merge branch 'v8.5'Pierre-Marie Pédrot
2016-05-09Rename Lexer -> CLexer.Pierre-Marie Pédrot
2016-03-20Moving Tactic_debug to Hightactic.Pierre-Marie Pédrot
2016-03-06Removing dependency of Himsg in tactic files.Pierre-Marie Pédrot
2016-03-06Moving Tactic_debug to tactics/ folder.Pierre-Marie Pédrot
2016-03-06Moving Ltac traces to Tacexpr and Tacinterp.Pierre-Marie Pédrot
2016-01-20Update copyright headers.Maxime Dénès
2015-05-18The Fail command does not catch uncaught exception anomalies anymore.Pierre-Marie Pédrot
2015-04-23Remove almost all the uses of string concatenation when building error messages.Guillaume Melquiond
2015-03-05Do not prepend a "Error:" header when the error is expected by the user.Guillaume Melquiond
2015-02-02Removing dead code.Pierre-Marie Pédrot
2015-01-17Univs: proper printing of global and local universe names (onlyMatthieu Sozeau
2015-01-12Update headers.Maxime Dénès
2014-12-16Getting rid of Exninfo hacks.Pierre-Marie Pédrot
2014-11-17Setting error tag on generic errors returned by Coqtop.Pierre-Marie Pédrot
2014-10-22Split [Proofview] into a file where the basic operations on the state are def...Arnaud Spiwack
2014-09-12Referring to evars by names. Added a parser for evars (but parsing ofHugo Herbelin
2014-08-04Cleaning of the new implementation of the tactic monad.Arnaud Spiwack
2014-07-01Fixing the place where to insert a space in "Tactic failure"Hugo Herbelin
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-02 14:40:24 +0000