coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Update headers following #6543.	Théo Zimmermann	2018-02-27
\|
*	[error] Replace msg_error by a proper exception.	Emilio Jesus Gallego Arias	2018-02-09
\| \| \| \| \| \| \| \| \| \|	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].
*	deprecate Pp.std_ppcmds type alias	Matej Košík	2017-07-27
\|
*	Bump year in headers.	Pierre-Marie Pédrot	2017-07-04
\|
*	Adding a bit of documentation in the mli.	Pierre-Marie Pédrot	2016-06-09
\|
*	Merge branch 'v8.5'	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
\|
*	Adding a primitive to the tactic monad to modify the exceptional content.	Pierre-Marie Pédrot	2015-05-07
\|
*	Exposing the minimal amount of internal of the Logic monad in order to	Pierre-Marie Pédrot	2015-05-06
\| \| \| \| \| \| \| \| \|	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.
*	Adding a new folder corresponding to the low-level part of the pretyper	Pierre-Marie Pédrot	2015-02-27
	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.