From b58961dc4485114212cc6948d0e966bf73087685 Mon Sep 17 00:00:00 2001
From: rustanleino <unknown>
Date: Fri, 19 Mar 2010 04:22:48 +0000
Subject: Dafny:  Ensures that function axioms are not being used while their
 consistency is being checked.

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

(limited to 'Binaries')

diff --git a/Binaries/DafnyPrelude.bpl b/Binaries/DafnyPrelude.bpl
index 50433b54..253cfd12 100644
--- a/Binaries/DafnyPrelude.bpl
+++ b/Binaries/DafnyPrelude.bpl
@@ -207,6 +207,13 @@ function DtRank(DatatypeType) returns (int);
 
 // ---------------------------------------------------------------
 
+// used to make sure function axioms are not used while their consistency is being checked
+const $ModuleContextHeight: int;
+const $FunctionContextHeight: int;
+const $InMethodContext: bool;
+
+// ---------------------------------------------------------------
+
 type Field alpha;
 type HeapType = <alpha>[ref,Field alpha]alpha;
 
-- 
cgit v1.2.3