summaryrefslogtreecommitdiff
path: root/Test/dafny2/COST-verif-comp-2011-1-MaxArray.dfy
diff options
context:
space:
mode:
authorGravatar Rustan Leino <unknown>2013-12-17 15:15:53 -0800
committerGravatar Rustan Leino <unknown>2013-12-17 15:15:53 -0800
commit69690cc00356be153b2598cce3abb228d1cc5a33 (patch)
tree3e1630a9dae215bd59610098e0d0a0425f280f65 /Test/dafny2/COST-verif-comp-2011-1-MaxArray.dfy
parent968d203bfd0254b496f93664303e84da9795d170 (diff)
Don't expand {:opaque} for inherited functions. (Note, more design is still needed to handle the combination of opaque and refinement well.)
Diffstat (limited to 'Test/dafny2/COST-verif-comp-2011-1-MaxArray.dfy')
0 files changed, 0 insertions, 0 deletions