From e12110637730d067c216abcc86185b761189b342 Mon Sep 17 00:00:00 2001
From: vblot <24938579+vblot@users.noreply.github.com>
Date: Fri, 28 May 2021 18:29:37 +0200
Subject: getting rid of native-coq (#95)

---
 src/trace/smtCertif.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

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

diff --git a/src/trace/smtCertif.ml b/src/trace/smtCertif.ml
index 2ea4ca8..24cdf78 100644
--- a/src/trace/smtCertif.ml
+++ b/src/trace/smtCertif.ml
@@ -98,11 +98,11 @@ type 'hform rule =
     *)
 
   (* Linear arithmetic *)
-  | LiaMicromega of 'hform list * Structures.Micromega_plugin_Certificate.Mc.zArithProof list
+  | LiaMicromega of 'hform list * CoqInterface.Micromega_plugin_Certificate.Mc.zArithProof list
   | LiaDiseq of 'hform
 
   (* Arithmetic simplifications *)
-  | SplArith of 'hform clause * 'hform * Structures.Micromega_plugin_Certificate.Mc.zArithProof list
+  | SplArith of 'hform clause * 'hform * CoqInterface.Micromega_plugin_Certificate.Mc.zArithProof list
 
   (* Elimination of operators *)
   | SplDistinctElim of 'hform clause * 'hform
-- 
cgit