index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
test-suite
/
ide
Commit message (
Expand
)
Author
Age
*
Farewell decl_mode
Enrico Tassi
2017-03-07
*
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
*
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
*
Future: blocking by default
Enrico Tassi
2014-12-17
*
fake_ide: ported to spawn
Enrico Tassi
2014-02-10
*
Document: undoing inside a focused zone does not require unfocusing
gareuselesinge
2013-10-10
*
fake_ide: ported to Document + 2 tests for editing a proof (locally)
gareuselesinge
2013-10-10
*
fake_ide: speak the new protocol
gareuselesinge
2013-10-07
*
Coqide ported to STM
gareuselesinge
2013-08-08
*
test-suite/ide: misc improvement
letouzey
2011-09-06
*
fake_ide: a short program to mimic an ide talking to coqtop -ideslave
letouzey
2011-09-05
*
Introducing strong typing for IDE - toplevel IPC
vgross
2010-05-31
*
Fix bug in backtracking.
vgross
2010-03-23
*
New backtracking code + fix bug #2082.
vgross
2010-02-26
*
- Correction bug highlighting "Module" dans Coqide
herbelin
2008-05-28
*
Correction bugs ide undo et highlight (suite à typos)
herbelin
2008-05-21
*
Léger backtrack sur commit coqide précédent (si la commande à annuler
herbelin
2008-05-20
*
Fixed coqide bug #1856 that was introduced in revision 10915.
herbelin
2008-05-20