diff options
| author |  Rustan Leino <unknown> | 2014-03-06 16:16:18 -0800 |
|---|---|---|
| committer | Rustan Leino <unknown> | 2014-03-06 16:16:18 -0800 |
| commit | dfe5b172bd5419a20487a03c6051ccac1e16edc1 (patch) | |
| tree | 891a77bd157b93f2b292e4eb71d0ffcf00d00ea3 /Binaries | |
| parent | efc11762c9d697aef9eae0cebd1d17aaf229d2a8 (diff) | |
Removed an apparently unneeded trigger.
Diffstat (limited to 'Binaries')
| -rw-r--r-- | Binaries/DafnyPrelude.bpl | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/Binaries/DafnyPrelude.bpl b/Binaries/DafnyPrelude.bpl index d4c97f0f..ffc6715b 100644 --- a/Binaries/DafnyPrelude.bpl +++ b/Binaries/DafnyPrelude.bpl @@ -605,7 +605,6 @@ axiom FDim(alloc) == 0 && !$IsGhostField(alloc); // treat as non-ghost field, b function DtAlloc(DatatypeType, HeapType): bool;
axiom (forall h, k: HeapType, d: DatatypeType ::
{ $HeapSucc(h, k), DtAlloc(d, h) }
- { $HeapSucc(h, k), DtAlloc(d, k) }
$HeapSucc(h, k) ==> DtAlloc(d, h) ==> DtAlloc(d, k));
function GenericAlloc(BoxType, HeapType): bool;
|