From 31f5a7c20e25225e4b9dca95e60e955402f64df6 Mon Sep 17 00:00:00 2001
From: rustanleino <unknown>
Date: Mon, 1 Nov 2010 21:56:14 +0000
Subject: Dafny: a partial first crack at a Dafny model-viewer provider,
 including captureState mark-ups in the Boogie code generated from Dafny

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

(limited to 'Binaries/DafnyPrelude.bpl')

diff --git a/Binaries/DafnyPrelude.bpl b/Binaries/DafnyPrelude.bpl
index 476a6bd9..5675d2a1 100644
--- a/Binaries/DafnyPrelude.bpl
+++ b/Binaries/DafnyPrelude.bpl
@@ -4,6 +4,9 @@
 // Edited sequence axioms 20 October 2009 by Alex Summers.
 // Copyright (c) 2008-2010, Microsoft.
 
+const $$Language$Dafny: bool;  // To be recognizable to the ModelViewer as
+axiom $$Language$Dafny;        // coming from a Dafny program.
+
 // ---------------------------------------------------------------
 // -- References -------------------------------------------------
 // ---------------------------------------------------------------
-- 
cgit v1.2.3