aboutsummaryrefslogtreecommitdiff
path: root/test-suite/ide
AgeCommit message (Expand)Author
2016-03-19Moving the parsing of the Ltac proof mode to G_ltac.Pierre-Marie Pédrot
2015-06-09STM: states coming from workers have no proof terminators (Close #4246)Enrico Tassi
2015-06-09STM: silly mistake in jumping back to an old state (Close #4249)Enrico Tassi
2015-05-28STM: preserve branch name on edit (Close: #4245, #4246)Enrico Tassi
2015-05-28Test for 4159Enrico Tassi
2015-03-11admit: replaced by give_up + Admitted (no proof_admitted : False, close #4032)Enrico Tassi
2014-12-17Future: blocking by defaultEnrico Tassi
2014-02-10fake_ide: ported to spawnEnrico Tassi
2013-10-10Document: undoing inside a focused zone does not require unfocusinggareuselesinge
2013-10-10fake_ide: ported to Document + 2 tests for editing a proof (locally)gareuselesinge
2013-10-07fake_ide: speak the new protocolgareuselesinge
2013-08-08Coqide ported to STMgareuselesinge
2011-09-06test-suite/ide: misc improvementletouzey
2011-09-05fake_ide: a short program to mimic an ide talking to coqtop -ideslaveletouzey
2010-05-31Introducing strong typing for IDE - toplevel IPCvgross
2010-03-23Fix bug in backtracking.vgross
2010-02-26New backtracking code + fix bug #2082.vgross
2008-05-28- Correction bug highlighting "Module" dans Coqideherbelin
2008-05-21Correction bugs ide undo et highlight (suite à typos)herbelin
2008-05-20Léger backtrack sur commit coqide précédent (si la commande à annulerherbelin
2008-05-20Fixed coqide bug #1856 that was introduced in revision 10915.herbelin