diff options
| author | Arnaud Spiwack | 2013-12-04 15:47:49 +0100 |
|---|---|---|
| committer | Arnaud Spiwack | 2013-12-04 15:47:49 +0100 |
| commit | 461edf898d34a4e735fcaed50645480d8cbd0f7f (patch) | |
| tree | 773a5ffcec4411d612a42f40dcd672550783636d | |
| parent | 078efbe2dfff0b783cd35b0b3ab2354f554e95a6 (diff) | |
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.
| -rw-r--r-- | toplevel/stm.ml | 1 |
1 files changed, 0 insertions, 1 deletions
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 |