diff options
| author |  Enrico Tassi <Enrico.Tassi@inria.fr> | 2015-03-15 18:32:22 +0100 |
|---|---|---|
| committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2015-03-15 18:48:48 +0100 |
| commit | e46afc2f884d3527c5a9826012b4ec7a58a43661 (patch) | |
| tree | 89b74adcff744f9eecae35855227b45a45b2a7d3 /stm | |
| parent | 1710356cdac3e968d678b75abb52d78a58b63e07 (diff) | |
STM: -quick: async no Proof using but no Section (#4124)
As happens in interactive mode.
Diffstat (limited to 'stm')
| -rw-r--r-- | stm/stm.ml | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/stm/stm.ml b/stm/stm.ml index 70e242bb5..b464b735b 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -1657,7 +1657,9 @@ let collect_proof keep cur hd brkind id = let t, v = proof_no_using last in v.expr <- VernacProof(t, Some hint); `ASync (parent last,proof_using_ast last,accn,name,delegate name) - with Not_found -> `Sync (no_name,None,`NoHint)) + with Not_found -> + let name = name ids in + `MaybeASync (parent last, None, accn, name, delegate name)) | `Fork((_, hd', GuaranteesOpacity, ids), _) -> assert (VCS.Branch.equal hd hd' || VCS.Branch.equal hd VCS.edit_branch); let name = name ids in |