From e9c7c508c1900e6195164d263c9249e3c7b56b51 Mon Sep 17 00:00:00 2001
From: leino <unknown>
Date: Sun, 5 Apr 2015 01:56:49 -0700
Subject: Fixed some bugs in override axioms (but still missing support for
 classes with type parameters). Resolve ClassDecl.TraitsTyp as types. Moved
 declaration of TraitParent and NoTraitAtAll to prelude.

---
 Binaries/DafnyPrelude.bpl | 7 +++++++
 1 file changed, 7 insertions(+)

(limited to 'Binaries')

diff --git a/Binaries/DafnyPrelude.bpl b/Binaries/DafnyPrelude.bpl
index 4972517b..74bdb63e 100644
--- a/Binaries/DafnyPrelude.bpl
+++ b/Binaries/DafnyPrelude.bpl
@@ -100,6 +100,13 @@ axiom (forall n: int ::
 type ref;
 const null: ref;
 
+// ---------------------------------------------------------------
+// -- Traits -----------------------------------------------------
+// ---------------------------------------------------------------
+
+const unique NoTraitAtAll: ClassName;
+function TraitParent(ClassName): ClassName;
+
 // ---------------------------------------------------------------
 // -- Boxing and unboxing ----------------------------------------
 // ---------------------------------------------------------------
-- 
cgit v1.2.3