coq - The formal proof system

Age	Commit message (Collapse)	Author
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-11-24	[lib] Generalize Control.timeout type.	Emilio Jesus Gallego Arias
	We also remove some internal implementation details from the mli file, there due historical reasons.
2017-07-04	Bump year in headers.	Pierre-Marie Pédrot

2016-08-19	Make the user_err header an optional parameter.	Emilio Jesus Gallego Arias
	Suggested by @ppedrot
2016-08-19	Remove errorlabstrm in favor of user_err	Emilio Jesus Gallego Arias
	As noted by @ppedrot, the first is redundant. The patch is basically a renaming. We didn't make the component optional yet, but this could happen in a future patch.
2016-07-03	errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib ↵	Pierre Letouzey
	module) For the moment, there is an Error module in compilers-lib/ocamlbytecomp.cm(x)a
2016-05-31	Feedback cleanup	Emilio Jesus Gallego Arias
	This patch splits pretty printing representation from IO operations. - `Pp` is kept in charge of the abstract pretty printing representation. - The `Feedback` module provides interface for doing printing IO. The patch continues work initiated for 8.5 and has the following effects: - The following functions in `Pp`: `pp`, `ppnl`, `pperr`, `pperrnl`, `pperr_flush`, `pp_flush`, `flush_all`, `msg`, `msgnl`, `msgerr`, `msgerrnl`, `message` are removed. `Feedback.msg_*` functions must be used instead. - Feedback provides different backends to handle output, currently, `stdout`, `emacs` and CoqIDE backends are provided. - Clients cannot specify flush policy anymore, thus `pp_flush` et al are gone. - `Feedback.feedback` takes an `edit_or_state_id` instead of the old mix. Lightly tested: Test-suite passes, Proof General and CoqIDE seem to work.
2016-05-08	Removing dead code and unused opens.	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-05-05	Merge branch 'v8.5'	Pierre-Marie Pédrot

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.