From 3fdc107b26f475c8fe8b7052de826405b88c14b3 Mon Sep 17 00:00:00 2001
From: QGarchery <QGarchery@users.noreply.github.com>
Date: Fri, 30 Nov 2018 09:06:02 +0100
Subject: forall declaration can now begin with a negation (#23)

Solves issue #21
---
 src/verit/veritParser.mly | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'src/verit/veritParser.mly')

diff --git a/src/verit/veritParser.mly b/src/verit/veritParser.mly
index 4ea6cd6..3c675ee 100644
--- a/src/verit/veritParser.mly
+++ b/src/verit/veritParser.mly
@@ -182,7 +182,7 @@ var_decl_list:
 ;
 
 forall_decl:
-  | FORALL LPAR var_decl_list RPAR name_term		   { clear_qvar (); false, Form (Fapp (Fforall $3, [|lit_of_atom_form_lit rf $5|])) }
+  | FORALL LPAR var_decl_list RPAR blit		   { clear_qvar (); false, Form (Fapp (Fforall $3, [|lit_of_atom_form_lit rf $5|])) }
 ; 
 
 term:   /* returns a bool * (SmtAtom.Form.pform or SmtAtom.hatom), the boolean indicates if we should declare the term or not */
-- 
cgit