From c2ce7fa6db14551fa49e1d7b46f795bd629c2061 Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Wed, 20 Jun 2018 13:20:56 +0100
Subject: Coq: port handling of effectful and/or from Lem backend

---
 lib/flow.sail | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'lib')

diff --git a/lib/flow.sail b/lib/flow.sail
index 7dc5969e..b698b597 100644
--- a/lib/flow.sail
+++ b/lib/flow.sail
@@ -2,6 +2,8 @@ $ifndef _FLOW
 $define _FLOW
 
 val not_bool = {coq: "negb", _: "not"} : bool -> bool
+/* NB: There are special cases in Sail for effectful uses of and_bool and
+   or_bool that are not shown here. */
 val and_bool = {coq: "andb", _: "and_bool"} : (bool, bool) -> bool
 val or_bool = {coq: "orb", _: "or_bool"} : (bool, bool) -> bool
 
-- 
cgit v1.2.3