aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/ltac
diff options
context:
space:
mode:
authorGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2017-07-20 17:10:58 +0200
committerGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2017-07-25 16:07:32 +0200
commitfc218c26cfb226be25c344af50b4b86e52360934 (patch)
treefd0650fa1fc981c81e62991d8d8e97431312285e /plugins/ltac
parentb6f3c8e4f173e3f272f966e1061e7112bf5d1b4a (diff)
[api] Remove type equalities from API.
This ensures that the API is self-contained and is, well, an API. Before this patch, the contents of `API.mli` bore little relation with what was used by the plugins [example: `Metasyntax` in tacentries.ml]. Many missing types had to be added. A sanity check of the `API.mli` file can be done with: `ocamlfind ocamlc -rectypes -package camlp5 -I lib API/API.mli`
Diffstat (limited to 'plugins/ltac')
-rw-r--r--plugins/ltac/extraargs.ml41
-rw-r--r--plugins/ltac/extraargs.mli1
-rw-r--r--plugins/ltac/extratactics.ml41
-rw-r--r--plugins/ltac/g_auto.ml41
-rw-r--r--plugins/ltac/g_ltac.ml42
-rw-r--r--plugins/ltac/g_obligations.ml41
-rw-r--r--plugins/ltac/g_rewrite.ml41
-rw-r--r--plugins/ltac/g_tactic.ml41
-rw-r--r--plugins/ltac/pltac.ml1
-rw-r--r--plugins/ltac/pltac.mli1
-rw-r--r--plugins/ltac/tacentries.ml1
-rw-r--r--plugins/ltac/tacentries.mli1
-rw-r--r--plugins/ltac/tacintern.ml1
-rw-r--r--plugins/ltac/tacintern.mli1
-rw-r--r--plugins/ltac/tacinterp.ml1
-rw-r--r--plugins/ltac/tacsubst.ml1
16 files changed, 0 insertions, 17 deletions
diff --git a/plugins/ltac/extraargs.ml4 b/plugins/ltac/extraargs.ml4
index 72c6f9090..609795133 100644
--- a/plugins/ltac/extraargs.ml4
+++ b/plugins/ltac/extraargs.ml4
@@ -8,7 +8,6 @@
(*i camlp4deps: "grammar/grammar.cma" i*)
-open Grammar_API
open Pp
open Genarg
open Stdarg
diff --git a/plugins/ltac/extraargs.mli b/plugins/ltac/extraargs.mli
index 419c5e8c4..acdf67779 100644
--- a/plugins/ltac/extraargs.mli
+++ b/plugins/ltac/extraargs.mli
@@ -6,7 +6,6 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-open Grammar_API
open Tacexpr
open Names
open Constrexpr
diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4
index 6d80ab549..f3f2f27e9 100644
--- a/plugins/ltac/extratactics.ml4
+++ b/plugins/ltac/extratactics.ml4
@@ -8,7 +8,6 @@
(*i camlp4deps: "grammar/grammar.cma" i*)
-open Grammar_API
open Pp
open Genarg
open Stdarg
diff --git a/plugins/ltac/g_auto.ml4 b/plugins/ltac/g_auto.ml4
index 4d13d89a4..301943a50 100644
--- a/plugins/ltac/g_auto.ml4
+++ b/plugins/ltac/g_auto.ml4
@@ -8,7 +8,6 @@
(*i camlp4deps: "grammar/grammar.cma" i*)
-open Grammar_API
open Pp
open Genarg
open Stdarg
diff --git a/plugins/ltac/g_ltac.ml4 b/plugins/ltac/g_ltac.ml4
index cc052c8a2..2ea0f60eb 100644
--- a/plugins/ltac/g_ltac.ml4
+++ b/plugins/ltac/g_ltac.ml4
@@ -8,8 +8,6 @@
(*i camlp4deps: "grammar/grammar.cma" i*)
-open Grammar_API
-
DECLARE PLUGIN "ltac_plugin"
open Util
diff --git a/plugins/ltac/g_obligations.ml4 b/plugins/ltac/g_obligations.ml4
index 1935d560a..1a2d89586 100644
--- a/plugins/ltac/g_obligations.ml4
+++ b/plugins/ltac/g_obligations.ml4
@@ -12,7 +12,6 @@
Syntax for the subtac terms and types.
Elaborated from correctness/psyntax.ml4 by Jean-Christophe Filliātre *)
-open Grammar_API
open Libnames
open Constrexpr
open Constrexpr_ops
diff --git a/plugins/ltac/g_rewrite.ml4 b/plugins/ltac/g_rewrite.ml4
index 3c27b2747..c874f8d5a 100644
--- a/plugins/ltac/g_rewrite.ml4
+++ b/plugins/ltac/g_rewrite.ml4
@@ -10,7 +10,6 @@
(* Syntax for rewriting with strategies *)
-open Grammar_API
open Names
open Misctypes
open Locus
diff --git a/plugins/ltac/g_tactic.ml4 b/plugins/ltac/g_tactic.ml4
index e539b5867..d792d4ff7 100644
--- a/plugins/ltac/g_tactic.ml4
+++ b/plugins/ltac/g_tactic.ml4
@@ -6,7 +6,6 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-open Grammar_API
open Pp
open CErrors
open Util
diff --git a/plugins/ltac/pltac.ml b/plugins/ltac/pltac.ml
index 2adcf02e6..2c1b1067e 100644
--- a/plugins/ltac/pltac.ml
+++ b/plugins/ltac/pltac.ml
@@ -6,7 +6,6 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-open Grammar_API
open Pcoq
(* Main entry for extensions *)
diff --git a/plugins/ltac/pltac.mli b/plugins/ltac/pltac.mli
index 794cb527f..048dcc8e9 100644
--- a/plugins/ltac/pltac.mli
+++ b/plugins/ltac/pltac.mli
@@ -8,7 +8,6 @@
(** Ltac parsing entries *)
-open Grammar_API
open Loc
open Names
open Pcoq
diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml
index 791b7f48d..cf676f598 100644
--- a/plugins/ltac/tacentries.ml
+++ b/plugins/ltac/tacentries.ml
@@ -6,7 +6,6 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-open Grammar_API
open Pp
open CErrors
open Util
diff --git a/plugins/ltac/tacentries.mli b/plugins/ltac/tacentries.mli
index ccd44b914..aa8f4efe6 100644
--- a/plugins/ltac/tacentries.mli
+++ b/plugins/ltac/tacentries.mli
@@ -8,7 +8,6 @@
(** Ltac toplevel command entries. *)
-open Grammar_API
open Vernacexpr
open Tacexpr
diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml
index df03c7b47..0554d4364 100644
--- a/plugins/ltac/tacintern.ml
+++ b/plugins/ltac/tacintern.ml
@@ -6,7 +6,6 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-open Grammar_API
open Pattern
open Pp
open Genredexpr
diff --git a/plugins/ltac/tacintern.mli b/plugins/ltac/tacintern.mli
index ad2e70908..b262473a9 100644
--- a/plugins/ltac/tacintern.mli
+++ b/plugins/ltac/tacintern.mli
@@ -6,7 +6,6 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-open Grammar_API
open Pp
open Names
open Tacexpr
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index 7b054947b..60a8f75ec 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -6,7 +6,6 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-open Grammar_API
open Constrintern
open Patternops
open Pp
diff --git a/plugins/ltac/tacsubst.ml b/plugins/ltac/tacsubst.ml
index c1ca85433..180fb2db4 100644
--- a/plugins/ltac/tacsubst.ml
+++ b/plugins/ltac/tacsubst.ml
@@ -6,7 +6,6 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-open Grammar_API
open Util
open Tacexpr
open Mod_subst