From 661940fd55a925a6f17f6025f5d15fc9f5647cf9 Mon Sep 17 00:00:00 2001 From: Matej Kosik Date: Mon, 10 Oct 2016 10:59:22 +0200 Subject: Put all plugins behind an "API". --- plugins/extraction/common.ml | 1 + plugins/extraction/common.mli | 1 + plugins/extraction/extract_env.ml | 1 + plugins/extraction/extract_env.mli | 1 + plugins/extraction/extraction.ml | 1 + plugins/extraction/extraction.mli | 1 + plugins/extraction/g_extraction.ml4 | 4 +++- plugins/extraction/haskell.ml | 1 + plugins/extraction/json.ml | 1 + plugins/extraction/miniml.mli | 1 + plugins/extraction/mlutil.ml | 1 + plugins/extraction/mlutil.mli | 1 + plugins/extraction/modutil.ml | 1 + plugins/extraction/modutil.mli | 1 + plugins/extraction/ocaml.ml | 1 + plugins/extraction/scheme.ml | 1 + plugins/extraction/table.ml | 1 + plugins/extraction/table.mli | 1 + 18 files changed, 20 insertions(+), 1 deletion(-) (limited to 'plugins/extraction') diff --git a/plugins/extraction/common.ml b/plugins/extraction/common.ml index c498eb589..9c3f97696 100644 --- a/plugins/extraction/common.ml +++ b/plugins/extraction/common.ml @@ -6,6 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open API open Pp open Util open Names diff --git a/plugins/extraction/common.mli b/plugins/extraction/common.mli index b8e95afb3..4c9b1e1a5 100644 --- a/plugins/extraction/common.mli +++ b/plugins/extraction/common.mli @@ -6,6 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open API open Names open Globnames open Miniml diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml index 2c85b185c..688bcd025 100644 --- a/plugins/extraction/extract_env.ml +++ b/plugins/extraction/extract_env.ml @@ -6,6 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open API open Miniml open Term open Declarations diff --git a/plugins/extraction/extract_env.mli b/plugins/extraction/extract_env.mli index 90f4f911b..1e7a6ba5b 100644 --- a/plugins/extraction/extract_env.mli +++ b/plugins/extraction/extract_env.mli @@ -8,6 +8,7 @@ (*s This module declares the extraction commands. *) +open API open Names open Libnames open Globnames diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml index 92ece7ccf..f1a50e7eb 100644 --- a/plugins/extraction/extraction.ml +++ b/plugins/extraction/extraction.ml @@ -7,6 +7,7 @@ (************************************************************************) (*i*) +open API open Util open Names open Term diff --git a/plugins/extraction/extraction.mli b/plugins/extraction/extraction.mli index cdda777a6..2b4b05a95 100644 --- a/plugins/extraction/extraction.mli +++ b/plugins/extraction/extraction.mli @@ -8,6 +8,7 @@ (*s Extraction from Coq terms to Miniml. *) +open API open Names open Term open Declarations diff --git a/plugins/extraction/g_extraction.ml4 b/plugins/extraction/g_extraction.ml4 index 3ed959cf2..6cba83ef9 100644 --- a/plugins/extraction/g_extraction.ml4 +++ b/plugins/extraction/g_extraction.ml4 @@ -8,6 +8,9 @@ (*i camlp4deps: "grammar/grammar.cma" i*) +open API +open Grammar_API.Pcoq.Prim + DECLARE PLUGIN "extraction_plugin" (* ML names *) @@ -15,7 +18,6 @@ DECLARE PLUGIN "extraction_plugin" open Ltac_plugin open Genarg open Stdarg -open Pcoq.Prim open Pp open Names open Nameops diff --git a/plugins/extraction/haskell.ml b/plugins/extraction/haskell.ml index eb13fd675..8cdfb3499 100644 --- a/plugins/extraction/haskell.ml +++ b/plugins/extraction/haskell.ml @@ -8,6 +8,7 @@ (*s Production of Haskell syntax. *) +open API open Pp open CErrors open Util diff --git a/plugins/extraction/json.ml b/plugins/extraction/json.ml index e43c47d05..1bf19f186 100644 --- a/plugins/extraction/json.ml +++ b/plugins/extraction/json.ml @@ -1,3 +1,4 @@ +open API open Pp open Util open Names diff --git a/plugins/extraction/miniml.mli b/plugins/extraction/miniml.mli index db3361522..28226f225 100644 --- a/plugins/extraction/miniml.mli +++ b/plugins/extraction/miniml.mli @@ -8,6 +8,7 @@ (*s Target language for extraction: a core ML called MiniML. *) +open API open Pp open Names open Globnames diff --git a/plugins/extraction/mlutil.ml b/plugins/extraction/mlutil.ml index 402fe4ffe..5a50899c6 100644 --- a/plugins/extraction/mlutil.ml +++ b/plugins/extraction/mlutil.ml @@ -7,6 +7,7 @@ (************************************************************************) (*i*) +open API open Util open Names open Libnames diff --git a/plugins/extraction/mlutil.mli b/plugins/extraction/mlutil.mli index c66755249..2655dfc89 100644 --- a/plugins/extraction/mlutil.mli +++ b/plugins/extraction/mlutil.mli @@ -6,6 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open API open Names open Globnames open Miniml diff --git a/plugins/extraction/modutil.ml b/plugins/extraction/modutil.ml index b67b9931e..2b1e81060 100644 --- a/plugins/extraction/modutil.ml +++ b/plugins/extraction/modutil.ml @@ -6,6 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open API open Names open Globnames open CErrors diff --git a/plugins/extraction/modutil.mli b/plugins/extraction/modutil.mli index dc8708249..45e890be0 100644 --- a/plugins/extraction/modutil.mli +++ b/plugins/extraction/modutil.mli @@ -6,6 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open API open Names open Globnames open Miniml diff --git a/plugins/extraction/ocaml.ml b/plugins/extraction/ocaml.ml index 4399fc561..83abaf508 100644 --- a/plugins/extraction/ocaml.ml +++ b/plugins/extraction/ocaml.ml @@ -8,6 +8,7 @@ (*s Production of Ocaml syntax. *) +open API open Pp open CErrors open Util diff --git a/plugins/extraction/scheme.ml b/plugins/extraction/scheme.ml index 3c81564e3..55168cc29 100644 --- a/plugins/extraction/scheme.ml +++ b/plugins/extraction/scheme.ml @@ -8,6 +8,7 @@ (*s Production of Scheme syntax. *) +open API open Pp open CErrors open Util diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml index 29dd8ff4f..607ca1b3a 100644 --- a/plugins/extraction/table.ml +++ b/plugins/extraction/table.ml @@ -6,6 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open API open Names open Term open Declarations diff --git a/plugins/extraction/table.mli b/plugins/extraction/table.mli index 15a08756c..cd1667bdb 100644 --- a/plugins/extraction/table.mli +++ b/plugins/extraction/table.mli @@ -6,6 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open API open Names open Libnames open Globnames -- cgit v1.2.3