From 461edf898d34a4e735fcaed50645480d8cbd0f7f Mon Sep 17 00:00:00 2001
From: Arnaud Spiwack
Date: Wed, 4 Dec 2013 15:47:49 +0100
Subject: Stm: remove an assertion.

In the code which indents proof scripts, you cannot assume that a single goal is closed at a time (because of dependent subgoals).

This change had been lost in the rebase over the paral-itp commits in october.---
 toplevel/stm.ml | 1 -
 1 file changed, 1 deletion(-)

diff --git a/toplevel/stm.ml b/toplevel/stm.ml
index de0ece06d3..ea9a85f51d 100644
--- a/toplevel/stm.ml
+++ b/toplevel/stm.ml
@@ -1771,7 +1771,6 @@ let indent_script_item ((ng1,ngl1),nl,beginend,ppl) (cmd,ng) =
     else if ng < ngprev then
       (* A subgoal have been solved. Let's compute the new current level
 	 by discarding all levels with 0 remaining goals. *)
-      let _ = assert (Int.equal ng (ngprev - 1)) in
       let rec loop = function
 	| (0, ng2::ngl2) -> loop (ng2,ngl2)
 	| p -> p
-- 
cgit v1.2.3