coq - The formal proof system

Age	Commit message (Collapse)	Author
2020-12-06	Add support for high resolution timeout functions.	Lasse Blaauwbroek

2020-11-22	Fix timeout by ensuring signal exceptions are not erroneously caught	Lasse Blaauwbroek
	Fixes #7430 and fixes #10968 This commit makes the following changes: - Add an exception `Signal` used to convert OCaml signals to exceptions. `Signal` is registered as critical in `CErrors` to avoid being caught in the wrong `with` clauses. - Make `Control.timeout` into a safer interface based on `option` instead of exceptions. - Modify `tclTIMEOUT` to fail with `CErrors.Timeout` instead of `Logic_monad.Tac_timeout`, as was already advertised in the ocamldoc documentation. - Removes `Logic_monad.Tac_timeout` altogether because it no longer has a use.
2020-03-18	Update headers in the whole code base.	Théo Zimmermann
	Add headers to a few files which were missing them.
2020-02-24	[exn] remove `raise` taking optional exception information argument	Emilio Jesus Gallego Arias
	This was redundant with `iraise`; exceptions in the logic monad now are forced to attach `info` to `Proofview.NonLogical.raise`
2019-08-27	[cleanup] Replace uses of UserError constructor, clarify exception names.	Emilio Jesus Gallego Arias
	We replace some uses of `raise (UserError ...)` with `CErrors.user_err`, ideally we would like to make the error raising API not depend on the exception themselves, but that's still a long way to go. We also rename the `Timeout` exception as to clarify purpose in the codebase, given that it has 3 different ones as of today. cc: #7560
2019-06-17	Update ml-style headers to new year.	Théo Zimmermann

2018-12-09	[doc] Enable Warning 50 [incorrect doc comment] and fix comments.	Emilio Jesus Gallego Arias
	This is a pre-requisite to use automated formatting tools such as `ocamlformat`, also, there were quite a few places where the comments had basically no effect, thus it was confusing for the developer. p.s: Reading some comments was a lot of fun :)
2018-02-27	Update headers following #6543.	Théo Zimmermann

2018-02-09	[error] Replace msg_error by a proper exception.	Emilio Jesus Gallego Arias
	The current error mechanism in the core part of Coq is 100% exception based; there was some confusion in the past as to whether raising and exception could be replace with `Feedback.msg_error`. As of today, this is not the case [due to some issues in the layer that generates error feedbacks in the STM] so all cases of `msg_error` must raise an exception of print at a different level [for now].
2017-07-27	deprecate Pp.std_ppcmds type alias	Matej Košík

2017-07-04	Bump year in headers.	Pierre-Marie Pédrot

2016-06-09	Adding a bit of documentation in the mli.	Pierre-Marie Pédrot

2016-01-21	Merge branch 'v8.5'	Pierre-Marie Pédrot

2015-10-19	Merge branch 'v8.5'	Pierre-Marie Pédrot

2015-10-06	Merge branch 'v8.5'	Pierre-Marie Pédrot

2015-05-07	Adding a primitive to the tactic monad to modify the exceptional content.	Pierre-Marie Pédrot

2015-05-06	Exposing the minimal amount of internal of the Logic monad in order to	Pierre-Marie Pédrot
	allow reusability of the implementation throughout the Coq codebase. We effectively feature a generalized version of the logical monad where the input state, the output state and the inner exception can be arbitrarily chosen. This will allow for more efficient implementations of close variants of the monad.
2015-02-27	Adding a new folder corresponding to the low-level part of the pretyper	Pierre-Marie Pédrot
	together with the tactic monad. The move is not complete yet, because some file candidates for this directory have almost useless dependencies in other ones that should not be moved.