From 41489a97014ab60b3dcc0f32dfdd10aacc6bcb98 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Wed, 14 Jun 2017 15:48:08 +0200
Subject: [API] Remove `open API` in ml files in favor of `-open API` flag.

---
 plugins/derive/derive.mli | 2 --
 1 file changed, 2 deletions(-)

(limited to 'plugins/derive/derive.mli')

diff --git a/plugins/derive/derive.mli b/plugins/derive/derive.mli
index 7ea64a5288..690a7c5083 100644
--- a/plugins/derive/derive.mli
+++ b/plugins/derive/derive.mli
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open API
-
 (** [start_deriving f suchthat lemma] starts a proof of [suchthat]
     (which can contain references to [f]) in the context extended by
     [f:=?x]. When the proof ends, [f] is defined as the value of [?x]
-- 
cgit v1.2.3