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/romega/const_omega.ml  | 1 -
 plugins/romega/const_omega.mli | 1 -
 plugins/romega/g_romega.ml4    | 1 -
 plugins/romega/refl_omega.ml   | 1 -
 4 files changed, 4 deletions(-)

(limited to 'plugins/romega')

diff --git a/plugins/romega/const_omega.ml b/plugins/romega/const_omega.ml
index 06c80a8256..4ffbd5aa8b 100644
--- a/plugins/romega/const_omega.ml
+++ b/plugins/romega/const_omega.ml
@@ -6,7 +6,6 @@
 
  *************************************************************************)
 
-open API
 open Names
 
 let module_refl_name = "ReflOmegaCore"
diff --git a/plugins/romega/const_omega.mli b/plugins/romega/const_omega.mli
index 6dc5d9f7e5..a452b1a917 100644
--- a/plugins/romega/const_omega.mli
+++ b/plugins/romega/const_omega.mli
@@ -6,7 +6,6 @@
 
  *************************************************************************)
 
-open API
 
 (** Coq objects used in romega *)
 
diff --git a/plugins/romega/g_romega.ml4 b/plugins/romega/g_romega.ml4
index 53f6f42c8e..5fd9c94194 100644
--- a/plugins/romega/g_romega.ml4
+++ b/plugins/romega/g_romega.ml4
@@ -8,7 +8,6 @@
 
 (*i camlp4deps: "grammar/grammar.cma" i*)
 
-open API
 
 DECLARE PLUGIN "romega_plugin"
 
diff --git a/plugins/romega/refl_omega.ml b/plugins/romega/refl_omega.ml
index 60e6e7de79..517df41d93 100644
--- a/plugins/romega/refl_omega.ml
+++ b/plugins/romega/refl_omega.ml
@@ -6,7 +6,6 @@
 
  *************************************************************************)
 
-open API
 open Pp
 open Util
 open Const_omega
-- 
cgit v1.2.3