From 98bf2facf5a61758897d000c4a7d1d6c6c2965fb Mon Sep 17 00:00:00 2001
From: Chantal Keller <Chantal.Keller@lri.fr>
Date: Sat, 30 Apr 2016 03:03:50 +0200
Subject: Holes in proof: - can now take learned clauses as argument - returns
 a whole clause (and not only a literal) - tested for the vernacular commands
 Warning: seems to slow down 8.5 version

---
 src/verit/veritLexer.mll | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'src/verit/veritLexer.mll')

diff --git a/src/verit/veritLexer.mll b/src/verit/veritLexer.mll
index 925ba92..2a51a02 100644
--- a/src/verit/veritLexer.mll
+++ b/src/verit/veritLexer.mll
@@ -95,7 +95,8 @@
         "tmp_qnt_tidy", TPQT;
         "tmp_qnt_simplify", TPQS;
         "tmp_skolemize", TPSK;
-        "subproof", SUBP ]
+        "subproof", SUBP;
+        "hole", HOLE ]
 }
 
 
-- 
cgit