diff options
| author | Emilio Jesus Gallego Arias | 2017-06-14 15:48:08 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2017-07-17 11:50:41 +0200 |
| commit | 41489a97014ab60b3dcc0f32dfdd10aacc6bcb98 (patch) | |
| tree | 652b04fc8b53d2f590151ec53f4b686f56fc694e /plugins/syntax | |
| parent | 99e84da08f7a38ac70d90d21d644b4a9a4a80c91 (diff) | |
[API] Remove `open API` in ml files in favor of `-open API` flag.
Diffstat (limited to 'plugins/syntax')
| -rw-r--r-- | plugins/syntax/ascii_syntax.ml | 1 | ||||
| -rw-r--r-- | plugins/syntax/int31_syntax.ml | 1 | ||||
| -rw-r--r-- | plugins/syntax/nat_syntax.ml | 1 | ||||
| -rw-r--r-- | plugins/syntax/r_syntax.ml | 1 | ||||
| -rw-r--r-- | plugins/syntax/string_syntax.ml | 1 | ||||
| -rw-r--r-- | plugins/syntax/z_syntax.ml | 1 |
6 files changed, 0 insertions, 6 deletions
diff --git a/plugins/syntax/ascii_syntax.ml b/plugins/syntax/ascii_syntax.ml index 6bf5b8cfca..c41ec39cb4 100644 --- a/plugins/syntax/ascii_syntax.ml +++ b/plugins/syntax/ascii_syntax.ml @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -open API (* Poor's man DECLARE PLUGIN *) let __coq_plugin_name = "ascii_syntax_plugin" diff --git a/plugins/syntax/int31_syntax.ml b/plugins/syntax/int31_syntax.ml index fe1eef866c..af64b1479a 100644 --- a/plugins/syntax/int31_syntax.ml +++ b/plugins/syntax/int31_syntax.ml @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open API (* Poor's man DECLARE PLUGIN *) let __coq_plugin_name = "int31_syntax_plugin" diff --git a/plugins/syntax/nat_syntax.ml b/plugins/syntax/nat_syntax.ml index c6ee899ed7..524a5c5221 100644 --- a/plugins/syntax/nat_syntax.ml +++ b/plugins/syntax/nat_syntax.ml @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open API (* Poor's man DECLARE PLUGIN *) let __coq_plugin_name = "nat_syntax_plugin" diff --git a/plugins/syntax/r_syntax.ml b/plugins/syntax/r_syntax.ml index 9cfa50071e..06117de79a 100644 --- a/plugins/syntax/r_syntax.ml +++ b/plugins/syntax/r_syntax.ml @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open API open Util open Names open Globnames diff --git a/plugins/syntax/string_syntax.ml b/plugins/syntax/string_syntax.ml index a4335a508b..b7f13b0400 100644 --- a/plugins/syntax/string_syntax.ml +++ b/plugins/syntax/string_syntax.ml @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -open API open Globnames open Ascii_syntax_plugin.Ascii_syntax open Glob_term diff --git a/plugins/syntax/z_syntax.ml b/plugins/syntax/z_syntax.ml index 719d8b1ccb..af3df28890 100644 --- a/plugins/syntax/z_syntax.ml +++ b/plugins/syntax/z_syntax.ml @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open API open Pp open CErrors open Util |