From d35b057995b4940af0e66bb081b3fe3ac7ff97f3 Mon Sep 17 00:00:00 2001
From: Chantal Keller <Chantal.Keller@lri.fr>
Date: Wed, 25 Sep 2019 18:22:53 +0200
Subject: Made SmtCommands independent from VeritSyntax Made lfsc/* mostly
 independent from VeritSyntax

---
 src/lfsc/tosmtcoq.mli | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'src/lfsc/tosmtcoq.mli')

diff --git a/src/lfsc/tosmtcoq.mli b/src/lfsc/tosmtcoq.mli
index b0d980b..34d3119 100644
--- a/src/lfsc/tosmtcoq.mli
+++ b/src/lfsc/tosmtcoq.mli
@@ -11,3 +11,6 @@
 
 
 include Translator_sig.S
+
+val ra : SmtAtom.Atom.reify_tbl
+val rf : SmtAtom.Form.reify
-- 
cgit