From e46afc2f884d3527c5a9826012b4ec7a58a43661 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <Enrico.Tassi@inria.fr>
Date: Sun, 15 Mar 2015 18:32:22 +0100
Subject: STM: -quick: async no Proof using but no Section (#4124)

As happens in interactive mode.
---
 stm/stm.ml | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

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
-- 
cgit v1.2.3