coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Farewell decl_mode	Enrico Tassi	2017-03-07
\| \| \| \| \|	This commit removes from the source tree plugins/decl_mode, its chapter in the reference manual and related tests.
*	Moving the parsing of the Ltac proof mode to G_ltac.	Pierre-Marie Pédrot	2016-03-19
\|
*	STM: states coming from workers have no proof terminators (Close #4246)	Enrico Tassi	2015-06-09
\| \| \| \|	Hence we reuse the ones in master.
*	STM: silly mistake in jumping back to an old state (Close #4249)	Enrico Tassi	2015-06-09
\|
*	STM: preserve branch name on edit (Close: #4245, #4246)	Enrico Tassi	2015-05-28
\|
*	Test for 4159	Enrico Tassi	2015-05-28
\|
*	admit: replaced by give_up + Admitted (no proof_admitted : False, close #4032)	Enrico Tassi	2015-03-11
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	- no more inconsistent Axiom in the Prelude - STM can now process Admitted proofs asynchronously - the quick chain can stock "Admitted" jobs in .vio files - the vio2vo step checks the jobs but does not stock the result in the opaque tables (they have no slot) - Admitted emits a warning if the proof is complete - Admitted uses the (partial) proof term to infer section variables used (if not given with Proof using), like for Qed - test-suite: extra line Require TestSuite.admit to each file making use of admit - test-suite/_CoqProject: to pass to CoqIDE and PG the right -Q flag to find TestSuite.admit
*	Future: blocking by default	Enrico Tassi	2014-12-17
\| \| \| \| \| \|	This makes queries like Print or Extraction block and not raise the error "the value is not ready". This should make CoqIDE work for every kind of script.
*	fake_ide: ported to spawn	Enrico Tassi	2014-02-10
\|
*	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
*	fake_ide: ported to Document + 2 tests for editing a proof (locally)	gareuselesinge	2013-10-10
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16871 85f007b7-540e-0410-9357-904b9bb8a0f7
*	fake_ide: speak the new protocol	gareuselesinge	2013-10-07
\| \| \| \| \| \| \| \| \|	A new syntax for .fake files, allowing multi line phrases and labeled script points (to go back to them). Test 7 fails because of a bug in STM (in a very spaghetti-like script). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16860 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Coqide ported to STM	gareuselesinge	2013-08-08
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Main changes for STM: 1) protocol changed to carry edit/state ids 2) colouring reflects the actual status of every span (evaluated or not) 3) button to force the evaluation of the whole buffer 4) cmd_stack and backtracking completely changed to use state numbers instead of counting sentences 5) feedback messages are completely asynchronous, and the whole protocol could be made so with a minor effort, but there is little point in it right now. Left as a future improvement. Missing bit: add sentence-id to responses of interp command. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16677 85f007b7-540e-0410-9357-904b9bb8a0f7
*	test-suite/ide: misc improvement	letouzey	2011-09-06
\| \| \| \| \| \| \|	- make clean really erases *.log - some missing \n at end of files git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14460 85f007b7-540e-0410-9357-904b9bb8a0f7
*	fake_ide: a short program to mimic an ide talking to coqtop -ideslave	letouzey	2011-09-05
\| \| \| \| \| \| \| \|	This way, we can test each night that coqtop -ideslave handles correctly some specific sequences of API calls. For the moment, we add a few tests of the backtracking. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14456 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Introducing strong typing for IDE - toplevel IPC	vgross	2010-05-31
\| \| \| \| \| \|	Obj.magic in toplevel/ide_blob.ml is the only way to simulate GADT. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13041 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fix bug in backtracking.	vgross	2010-03-23
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12876 85f007b7-540e-0410-9357-904b9bb8a0f7
*	New backtracking code + fix bug #2082.	vgross	2010-02-26
\| \| \| \| \| \|	Previous code checkings were too lax, and information was lost. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12823 85f007b7-540e-0410-9357-904b9bb8a0f7
*	- Correction bug highlighting "Module" dans Coqide	herbelin	2008-05-28
\| \| \| \| \| \| \| \| \|	- Divers code mort (evarutil.ml, Bvector.v) - MAJ perf-analysis git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11004 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Correction bugs ide undo et highlight (suite à typos)	herbelin	2008-05-21
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10957 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Léger backtrack sur commit coqide précédent (si la commande à annuler	herbelin	2008-05-20
\| \| \| \| \| \| \| \| \|	à potentiellement modifié l'état, on ne peut se contenter d'un Abort : il faut revenir au dernier état connu). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10951 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fixed coqide bug #1856 that was introduced in revision 10915.	herbelin	2008-05-20
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10950 85f007b7-540e-0410-9357-904b9bb8a0f7