From ec41af7ac01cef7c30785e6dd704381f31e7c2d3 Mon Sep 17 00:00:00 2001
From: ckeller <ckeller@users.noreply.github.com>
Date: Thu, 14 Feb 2019 20:09:40 +0100
Subject: V8.7 (#36)

Port SMTCoq to Coq-8.7
---
 src/lia/lia.ml | 9 ++-------
 1 file changed, 2 insertions(+), 7 deletions(-)

(limited to 'src/lia/lia.ml')

diff --git a/src/lia/lia.ml b/src/lia/lia.ml
index adeed4e..d8ed560 100644
--- a/src/lia/lia.ml
+++ b/src/lia/lia.ml
@@ -11,11 +11,6 @@
 
 
 (*** Linking SMT Terms to Micromega Terms ***)
-open Term
-open Coqlib
-open Declare
-open Decl_kinds
-open Entries
 open Util
 open Structures.Micromega_plugin_Micromega
 open Structures.Micromega_plugin_Coq_micromega
@@ -114,7 +109,7 @@ let smt_binop_to_micromega_formula tbl op ha hb =
   let rhs = smt_Atom_to_micromega_pExpr tbl hb in
   {flhs = lhs; fop = op; frhs = rhs }
 
-let rec smt_Atom_to_micromega_formula tbl ha =
+let smt_Atom_to_micromega_formula tbl ha =
   match Atom.atom ha with
     | Abop (op,ha,hb) -> smt_binop_to_micromega_formula tbl op ha hb
     | _ -> Structures.error
@@ -122,7 +117,7 @@ let rec smt_Atom_to_micromega_formula tbl ha =
 
 (* specialized fold *)
 
-let default_constr = mkInt 0
+let default_constr = Structures.econstr_of_constr (mkInt 0)
 let default_tag = Structures.Micromega_plugin_Mutils.Tag.from 0
 (* morphism for general formulas *)
 
-- 
cgit