From 041e5eef89b1db909f076494204eda2c20562bb8 Mon Sep 17 00:00:00 2001
From: Chantal Keller <Chantal.Keller@lri.fr>
Date: Tue, 3 Oct 2017 10:49:12 +0200
Subject: Compiles with Coq-8.6

---
 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 f39bff4..868a311 100644
--- a/src/trace/smtCertif.ml
+++ b/src/trace/smtCertif.ml
@@ -99,11 +99,11 @@ type 'hform rule =
     *)
 
   (* Linear arithmetic *)
-  | LiaMicromega of 'hform list * Certificate.Mc.zArithProof list
+  | LiaMicromega of 'hform list * Micromega_plugin.Certificate.Mc.zArithProof list
   | LiaDiseq of 'hform
 
   (* Arithmetic simplifications *)
-  | SplArith of 'hform clause * 'hform * Certificate.Mc.zArithProof list
+  | SplArith of 'hform clause * 'hform * Micromega_plugin.Certificate.Mc.zArithProof list
 
   (* Elimination of operators *)
   | SplDistinctElim of 'hform clause * 'hform
-- 
cgit