aboutsummaryrefslogtreecommitdiff
path: root/kernel/type_errors.mli
diff options
context:
space:
mode:
authorEnrico Tassi2016-02-15 16:11:11 +0100
committerEnrico Tassi2016-02-19 11:52:00 +0100
commit4f640bb24dfc45699670f41441355cdf71c83130 (patch)
tree77e76f3a2aec5a9a8065b4a35f630d7644c03ff6 /kernel/type_errors.mli
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 'kernel/type_errors.mli')
0 files changed, 0 insertions, 0 deletions