coq - The formal proof system

Age	Commit message (Collapse)	Author
2020-06-02	Move CoqIDE to its own folder	Maxime Dénès
	The will make it possible to put a VsCoq toplevel in `ide/vscoq`.
2020-03-18	Update headers in the whole code base.	Théo Zimmermann
	Add headers to a few files which were missing them.
2019-11-21	[coq] Untabify the whole ML codebase.	Emilio Jesus Gallego Arias
	We also remove trailing whitespace. Script used: ```bash for i in `find . -name '.ml' -or -name '.mli' -or -name '.mlg'`; do expand -i "$i" \| sponge "$i"; sed -e's/[[:space:]]$//' -i.bak "$i"; done ```
2019-06-17	Update ml-style headers to new year.	Théo Zimmermann

2018-02-27	Update headers following #6543.	Théo Zimmermann

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

2016-02-20	Fixing bug #4540: CoqIDE bottom progress bar does not update.	Pierre-Marie Pédrot

2016-01-02	Remove some unused functions.	Guillaume Melquiond
	Note: they do not even seem to have a debugging purpose, so better remove them before they bitrot.
2016-01-02	Avoid warnings about loop indices.	Guillaume Melquiond

2015-01-05	Removing GUtil dependency from ide/document.ml.	Pierre-Marie Pédrot
	We reimplement a quick-n-dirty Gtk-free signal handler.
2015-01-05	Implementing a segment-viewer in CoqIDE.	Pierre-Marie Pédrot
	This allows a nifty display of the current state of the document through a dedicated progress bar. Also closes bug #3764.
2013-10-24	CoqIDE: fix coloring bug when jumping back to the first phrase	gareuselesinge
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16928 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-10	Document: undoing inside a focused zone does not require unfocusing	gareuselesinge
	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
2013-10-10	CoqIDE: move cmd_stack to a separate module: Document	gareuselesinge
	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
2013-10-07	CoqIDE: cStack -> Document	gareuselesinge
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16856 85f007b7-540e-0410-9357-904b9bb8a0f7