coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Removing dead code and unused opens.	Pierre-Marie Pédrot	2016-05-08
\|
*	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-01-21
\|\
\| *	Update copyright headers.	Maxime Dénès	2016-01-20
\| \|
* \|	Remove some unused functions.	Guillaume Melquiond	2016-01-02
\| \| \| \| \| \| \| \| \| \|	Note: they do not even seem to have a debugging purpose, so better remove them before they bitrot.
* \|	Rich printing of goals.	Pierre-Marie Pédrot	2015-09-20
\| \|
* \|	Switching to an event-based mechanism for CoqIDE preferences.	Pierre-Marie Pédrot	2015-08-31
\| \| \| \| \| \| \| \| \| \|	There is no remaining hook in the preferences. In particular, the refresh_editor_hook is gone.
* \|	Using the new preference mechanism for colors in CoqIDE.	Pierre-Marie Pédrot	2015-08-16
\|/ \| \| \| \|	A lot of legacy code has been removed in the process in favour of signal-based interactions.
*	Make end-of-proof output consistent across toplevels.	Guillaume Melquiond	2015-06-19
\| \| \| \| \|	Ideally, the code should be shared between the various toplevels, but this is a lot more work than just fixing a few strings.
*	Compatibility ocaml 3.12.	Hugo Herbelin	2015-05-05
\|
*	Granting wish #4221.	Pierre-Marie Pédrot	2015-05-05
\|
*	Selecting whole words on double-click in CoqIDE.	Pierre-Marie Pédrot	2015-02-15
\| \| \| \|	Fixes bug #4026.
*	Selection of the current word in CoqIDE looks at all buffers.	Pierre-Marie Pédrot	2015-02-13
\|
*	Update headers.	Maxime Dénès	2015-01-12
\|
*	ide/wg_ProofView: Do not refer to the {Proof} internal module, use ↵	Regis-Gianas	2014-11-04
\| \| \| \|	{Interface} instead.
*	Factored out IDE goal structure.	Carst Tankink	2014-10-01
\| \| \| \| \| \| \| \| \| \| \| \|	The more structured goal record type of CoqIDE is also useful for other interfaces (in particular, for PIDE). To support this, the datatype was factored out to the Proof module. In addition, the record gains a type parameter, to allow interfaces to adapt the output to their needs. To accommodate this type, the Proof module also gains the map_structured_proof that takes a Proof.proof and a function on the individual goals (in the context of an evar map) and produces a structured goal based on the goal transformer.
*	Adds a tactic give_up.	aspiwack	2013-11-02
\| \| \| \| \| \|	Gives up on the focused goals. Shows an unsafe status. Unlike the admit tactic, the proof cannot be closed until the users goes back and solves these goals. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17018 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Adds a shelve tactic.	aspiwack	2013-11-02
\| \| \| \| \| \|	The shelve tactic puts all the focused goals out of sight. They can be later recalled by the Unshelve command. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17013 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Granting wish #1781:	ppedrot	2013-07-30
\| \| \| \| \| \|	Parenthesis matching on click in all term displays. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16643 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Moving Utils.list_* to a proper CList module, which includes stdlib	ppedrot	2012-09-14
\| \| \| \| \| \| \| \| \|	List module. That way, an "open Util" in the header permits using any function of CList in the List namespace (and in particular, this permits optimized reimplementations of the List functions, as, for example, tail-rec implementations. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15801 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Updating headers.	herbelin	2012-08-08
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15715 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Added abstration layer to goal display in CoqIDE, and cleaned parts	ppedrot	2012-07-16
	of the code altogether. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15623 85f007b7-540e-0410-9357-904b9bb8a0f7