diff options
Diffstat (limited to 'stm/stm.ml')
| -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 70e242bb54..b464b735bd 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 |