aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping
diff options
context:
space:
mode:
authorGravatar gareuselesinge <gareuselesinge@85f007b7-540e-0410-9357-904b9bb8a0f7>2013-10-07 16:17:51 +0000
committerGravatar gareuselesinge <gareuselesinge@85f007b7-540e-0410-9357-904b9bb8a0f7>2013-10-07 16:17:51 +0000
commit3c7971f7587b488ed709443aba8427330ea972b6 (patch)
tree6f033d2373cd843201256e7909b0f9c3437c6f74 /pretyping
parentb9c20bd3e59ae11d4994cb3ec9d908ca18677807 (diff)
fake_ide: speak the new protocol
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
Diffstat (limited to 'pretyping')
0 files changed, 0 insertions, 0 deletions