From d2f702da3b5cc9934f8cd3ea457f93c6ce2b6c12 Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Wed, 12 Jun 2019 17:25:47 +0100
Subject: Add AST for greater-than and less-than constraints Mostly to make
 constraints sent to the SMT solver and Coq nicer, but also makes it easy to
 remove uninformative constraints in the Coq back-end.

---
 language/sail.ott | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'language')

diff --git a/language/sail.ott b/language/sail.ott
index 8ef2babf..eb77e4aa 100644
--- a/language/sail.ott
+++ b/language/sail.ott
@@ -249,7 +249,9 @@ n_constraint :: 'NC_' ::=
   {{ aux _ l }}
   | nexp == nexp'                    :: :: equal
   | nexp >= nexp'                    :: :: bounded_ge
+  | nexp > nexp'                     :: :: bounded_gt
   | nexp '<=' nexp'                  :: :: bounded_le
+  | nexp '<' nexp'                   :: :: bounded_lt
   | nexp != nexp'                    :: :: not_equal
   | kid 'IN' { num1 , ... , numn }   :: :: set
   | n_constraint & n_constraint'     :: :: or
-- 
cgit v1.2.3