aboutsummaryrefslogtreecommitdiff
path: root/plugins/syntax/string_syntax.ml
diff options
context:
space:
mode:
authorPierre-Marie Pédrot2017-07-13 18:26:44 +0200
committerPierre-Marie Pédrot2017-07-13 19:36:20 +0200
commit0411c7e08b58edc4785c2be396fad0a037056a11 (patch)
tree83ed6ba9164ebca35aa802fe27973ae12816bc43 /plugins/syntax/string_syntax.ml
parenta59bdc4144476c0794ff24fc6180e21671842395 (diff)
Removing a use of AUContext.instance in the STM.
We only delay monomorphic proofs in quick mode, so that their universe context will always be empty.
Diffstat (limited to 'plugins/syntax/string_syntax.ml')
0 files changed, 0 insertions, 0 deletions