diff options
| author | Enrico Tassi | 2015-07-30 14:35:15 +0200 |
|---|---|---|
| committer | Enrico Tassi | 2015-07-30 14:35:20 +0200 |
| commit | 63ecb7386ae6e705d3f5577e01ec543f706c9427 (patch) | |
| tree | ea7119302e3657a4630994f0b839af801a40d9f3 | |
| parent | 5d0ff1782ab54914e7b0e5a736922aa297d327c8 (diff) | |
STM: make multiple, admitted, nested proofs work (fix #4314)
| -rw-r--r-- | stm/stm.ml | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/stm/stm.ml b/stm/stm.ml index ee12e48d5d..bf91c3aa4f 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -1858,9 +1858,8 @@ let known_state ?(redefine_qed=false) ~cache id = Some(Proof_global.close_proof ~keep_body_ucst_separate:false (State.exn_on id ~valid:eop)) in - reach view.next; - if keep == VtKeepAsAxiom then - Option.iter (vernac_interp id) pua; + if keep != VtKeepAsAxiom then + reach view.next; let wall_clock2 = Unix.gettimeofday () in vernac_interp id ?proof x; let wall_clock3 = Unix.gettimeofday () in |