From 52980aab9541a12619eb9191a94e9b2ba4684447 Mon Sep 17 00:00:00 2001
From: vblot <24938579+vblot@users.noreply.github.com>
Date: Fri, 28 May 2021 17:28:25 +0200
Subject: Get rid of most of our copy of micromega's source code (#94)

---
 src/versions/native/structures.ml  | 2 --
 src/versions/native/structures.mli | 2 --
 2 files changed, 4 deletions(-)

(limited to 'src/versions/native')

diff --git a/src/versions/native/structures.ml b/src/versions/native/structures.ml
index 0738801..435a1a1 100644
--- a/src/versions/native/structures.ml
+++ b/src/versions/native/structures.ml
@@ -140,9 +140,7 @@ let mkTrace step_to_coq next carray _ _ _ _ size step def_step r =
 
 (* Micromega *)
 module Micromega_plugin_Micromega = Micromega
-module Micromega_plugin_Mutils = Mutils
 module Micromega_plugin_Certificate = Certificate
-module Micromega_plugin_Coq_micromega = Coq_micromega
 
 let micromega_coq_proofTerm =
   Coq_micromega.M.coq_proofTerm
diff --git a/src/versions/native/structures.mli b/src/versions/native/structures.mli
index d8071d9..f2775a6 100644
--- a/src/versions/native/structures.mli
+++ b/src/versions/native/structures.mli
@@ -82,9 +82,7 @@ val mkTrace :
 
 (* Micromega *)
 module Micromega_plugin_Micromega = Micromega
-module Micromega_plugin_Mutils = Mutils
 module Micromega_plugin_Certificate = Certificate
-module Micromega_plugin_Coq_micromega = Coq_micromega
 
 val micromega_coq_proofTerm : constr lazy_t
 val micromega_dump_proof_term : Micromega_plugin_Certificate.Mc.zArithProof -> constr
-- 
cgit