From 6ba69eb95dfbf199d4929d6ee3054e26102b1f95 Mon Sep 17 00:00:00 2001
From: vgross
Date: Fri, 12 Feb 2010 17:50:36 +0000
Subject: Simplify backtracking

As we can now jump right onto a closed segment, there is no need for
complicated pattern matching.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12758 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 library/lib.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'library')

diff --git a/library/lib.ml b/library/lib.ml
index 65dcc83394..9c11cd991e 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -630,7 +630,7 @@ let reset_to_state sp =
   let (_,eq,before) = split_lib sp in
   (* if eq a frozen state, we'll reset to it *)
   match eq with
-  | [_,FrozenState f] -> lib_stk := eq@before;  unfreeze_summaries f
+  | [_,FrozenState f] -> lib_stk := eq@before; recalc_path_prefix (); unfreeze_summaries f
   | _ -> error "Not a frozen state"
 
 
-- 
cgit v1.2.3