diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-07-10 08:02:31 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-07-10 08:02:31 +0000 |
| commit | ddd8effe9fbee719e3a2d07f8338995d963ff630 (patch) | |
| tree | e9a544dca2cb4cd61f3b11ec862f1a32e376af61 /ide/coq.ml | |
| parent | 51f2cb48afad343834b299fa95046213a6826271 (diff) | |
Bug résiduel du backtrack de coqide se produisant lorsque la limite de
la pile de undo de tactique est atteinte (il ne fallait pas oublier de
faire un abort). On en profite pour porter cette limite à une valeur
significativement plus élevée.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11219 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'ide/coq.ml')
| -rw-r--r-- | ide/coq.ml | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/ide/coq.ml b/ide/coq.ml index 44dac6a94..61e223875 100644 --- a/ide/coq.ml +++ b/ide/coq.ml @@ -44,6 +44,8 @@ let init () = messages *) (**) Flags.make_silent true; + (* don't set a too large undo stack because Edit.create allocates an array *) + Pfedit.set_undo (Some 5000); (**) Coqtop.init_ide () |