From dfe5b172bd5419a20487a03c6051ccac1e16edc1 Mon Sep 17 00:00:00 2001
From: Rustan Leino <unknown>
Date: Thu, 6 Mar 2014 16:16:18 -0800
Subject: Removed an apparently unneeded trigger.

---
 Binaries/DafnyPrelude.bpl | 1 -
 1 file changed, 1 deletion(-)

(limited to 'Binaries')

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;
-- 
cgit v1.2.3