diff options
| author | gareuselesinge | 2013-08-09 08:58:29 +0000 |
|---|---|---|
| committer | gareuselesinge | 2013-08-09 08:58:29 +0000 |
| commit | ed18331f31fe2da5215a2548527e2b877f0b722f (patch) | |
| tree | 61b7e6cd2366072434abe7d6e20442ab99b86dee | |
| parent | 6410e8c242d50eb0571d0e6feea4526979c8b0b2 (diff) | |
fix batch compilation of scripts containing Admitted
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16689 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | toplevel/stm.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/toplevel/stm.ml b/toplevel/stm.ml index 7e8f64a019..70343c216e 100644 --- a/toplevel/stm.ml +++ b/toplevel/stm.ml @@ -980,7 +980,8 @@ let join_aborted_proofs () = if id = initial_state_id then () else let view = VCS.visit id in match view.step with - | `Qed ((_,VtDrop,_),eop) -> observe eop; aux view.next + | `Qed ((_,VtDrop,_),eop) -> + observe eop; Proof_global.discard_all (); aux view.next | `Sideff _ | `Alias _ | `Cmd _ | `Fork _ | `Qed _ -> aux view.next in aux (VCS.get_branch_pos VCS.master) |