aboutsummaryrefslogtreecommitdiffhomepage
path: root/ide/session.ml
diff options
context:
space:
mode:
authorGravatar Enrico Tassi <Enrico.Tassi@inria.fr>2016-02-15 16:11:11 +0100
committerGravatar Enrico Tassi <Enrico.Tassi@inria.fr>2016-02-19 11:52:00 +0100
commit4f640bb24dfc45699670f41441355cdf71c83130 (patch)
tree77e76f3a2aec5a9a8065b4a35f630d7644c03ff6 /ide/session.ml
parent8a179389fe5199e79d05b2c72ff2aae2061820aa (diff)
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.
Diffstat (limited to 'ide/session.ml')
0 files changed, 0 insertions, 0 deletions