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/trace/coqTerms.ml | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'src/trace/coqTerms.ml')

diff --git a/src/trace/coqTerms.ml b/src/trace/coqTerms.ml
index f2c24b8..a58fcfa 100644
--- a/src/trace/coqTerms.ml
+++ b/src/trace/coqTerms.ml
@@ -104,6 +104,8 @@ let smt_modules = [ ["SMTCoq";"Misc"];
 		    ["SMTCoq";"SMT_terms";"Atom"]
 		  ]
 
+let cState_C_t = gen_constant [["SMTCoq";"State";"C"]] "t"
+
 let cdistinct = gen_constant smt_modules "distinct"
 
 let ctype = gen_constant smt_modules "type"
-- 
cgit