aboutsummaryrefslogtreecommitdiffhomepage
path: root/ide/coqide.ml
diff options
context:
space:
mode:
authorGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2012-12-07 16:39:47 +0000
committerGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2012-12-07 16:39:47 +0000
commit2965635533740a4a0fb13a6f0390d56b4321b981 (patch)
tree23c6db9eb6ba8bfbc72e7e12960e2ae65a49c000 /ide/coqide.ml
parentce359ab8e44ad3df5b6f9eb27125e405b987f068 (diff)
Coqide: missing arg when calling process_next_phrase
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16041 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'ide/coqide.ml')
-rw-r--r--ide/coqide.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/ide/coqide.ml b/ide/coqide.ml
index af60b335b..de04e0891 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -1439,7 +1439,7 @@ let do_or_activate f =
do_if_not_computing p "do_or_activate"
(fun handle ->
let av = p.analyzed_view in
- ignore (f handle av);
+ f handle av;
pop_info ();
let msg = match Coq.status handle with
| Interface.Fail (l, str) ->
@@ -1463,7 +1463,7 @@ let do_if_active f =
(fun handle -> ignore (f handle p.analyzed_view))
module Nav = struct
- let forward_one _ = do_or_activate (fun h a -> a#process_next_phrase h)
+ let forward_one _ = do_or_activate (fun h a -> a#process_next_phrase h true)
let backward_one _ = do_or_activate (fun h a -> a#backtrack_last_phrase h)
let goto _ = do_or_activate (fun h a -> a#go_to_insert h)
let restart _ = force_reset_initial ()