diff options
author | Enrico Tassi <Enrico.Tassi@inria.fr> | 2016-02-15 16:11:11 +0100 |
---|---|---|
committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2016-02-19 11:52:00 +0100 |
commit | 4f640bb24dfc45699670f41441355cdf71c83130 (patch) | |
tree | 77e76f3a2aec5a9a8065b4a35f630d7644c03ff6 /ide/coqide.ml | |
parent | 8a179389fe5199e79d05b2c72ff2aae2061820aa (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/coqide.ml')
0 files changed, 0 insertions, 0 deletions