From 4f640bb24dfc45699670f41441355cdf71c83130 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Mon, 15 Feb 2016 16:11:11 +0100
Subject: STM: classify some variants of Instance as regular `Fork nodes.

"Instance name : Type." is like "Lemma name : Type", i.e. it starts
a proof.  Unfortunately sometimes it does not, so we say VtUnknown.
Still, if there is an open proof, we classify it as a regular Lemma,
i.e. the opacity depends only on the terminator.

This makes CoqIDE and PIDE based UI way more responsive when processing
files containing Instance that are proved by tactics, since they are now
correctly delegated to workers.  Bug reported privately by Alec Faithfull.
---
 stm/stm.ml | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

diff --git a/stm/stm.ml b/stm/stm.ml
index 56dcda6a4a..f2855d5087 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -2254,7 +2254,11 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty verbose c (loc, expr) =
                Proof_global.there_are_pending_proofs ()
             then begin
               let bname = VCS.mk_branch_name x in
-              VCS.commit id (Fork (x,bname,Doesn'tGuaranteeOpacity,[]));
+              let opacity_of_produced_term =
+                match x.expr with
+                | VernacInstance (false, _,_ , None, _) -> GuaranteesOpacity
+                | _ -> Doesn'tGuaranteeOpacity in
+              VCS.commit id (Fork (x,bname,opacity_of_produced_term,[]));
               VCS.branch bname (`Proof ("Classic", VCS.proof_nesting () + 1));
               Proof_global.activate_proof_mode "Classic";
             end else begin
-- 
cgit v1.2.3