coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Removing GUtil dependency from ide/document.ml.	Pierre-Marie Pédrot	2015-01-05
\| \| \| \|	We reimplement a quick-n-dirty Gtk-free signal handler.
*	Implementing a segment-viewer in CoqIDE.	Pierre-Marie Pédrot	2015-01-05
\| \| \| \| \| \| \|	This allows a nifty display of the current state of the document through a dedicated progress bar. Also closes bug #3764.
*	CoqIDE: fix coloring bug when jumping back to the first phrase	gareuselesinge	2013-10-24
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16928 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Document: undoing inside a focused zone does not require unfocusing	gareuselesinge	2013-10-10
\| \| \| \| \| \| \| \| \| \| \| \| \|	To test this fake_ide has also been improved with the GOALS command. As for CoqIDE, ADDing a sentence does not force its evaluation. The "advance 1 sentence" button is an ADD + GOALS. If one of the ADDed sentences is wrong, GOALS receives the error. The GUI then backtracks to a safe state id (sent by Coq). fake_ide has GOALS (asserts that the goals call was OK) and FAILGOALS to assert it fails and backtrack to a valid state. see unfdo022.fake. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16873 85f007b7-540e-0410-9357-904b9bb8a0f7
*	CoqIDE: move cmd_stack to a separate module: Document	gareuselesinge	2013-10-10
\| \| \| \| \| \| \| \|	The idea is to move the logic related to document handling to a separate module that can be tested by fake_ide too. CoqOps should "only" interface Document with the GtkTextBuffer. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16870 85f007b7-540e-0410-9357-904b9bb8a0f7
*	CoqIDE: cStack -> Document	gareuselesinge	2013-10-07
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16856 85f007b7-540e-0410-9357-904b9bb8a0f7