From 7351bf1c179c4feebf4d93437625ea358dc59420 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Sat, 11 Jul 2015 23:49:31 +0200
Subject: CoqIDE: recenter on backtrack (Close: #4277)

---
 ide/coqOps.ml | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/ide/coqOps.ml b/ide/coqOps.ml
index 2387d65c30..c6d3149475 100644
--- a/ide/coqOps.ml
+++ b/ide/coqOps.ml
@@ -669,7 +669,10 @@ object(self)
       push_info "Coq is undoing" in
     let conclusion () =
       pop_info ();
-      if move_insert then buffer#place_cursor ~where:self#get_start_of_input;
+      if move_insert then begin
+        buffer#place_cursor ~where:self#get_start_of_input;
+        script#recenter_insert;
+      end;
       let start = self#get_start_of_input in
       let stop = self#get_end_of_input in
       Minilib.log(Printf.sprintf "cleanup tags %d %d" start#offset stop#offset);
-- 
cgit v1.2.3