aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/ssr
diff options
context:
space:
mode:
authorGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2017-06-14 15:48:08 +0200
committerGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2017-07-17 11:50:41 +0200
commit41489a97014ab60b3dcc0f32dfdd10aacc6bcb98 (patch)
tree652b04fc8b53d2f590151ec53f4b686f56fc694e /plugins/ssr
parent99e84da08f7a38ac70d90d21d644b4a9a4a80c91 (diff)
[API] Remove `open API` in ml files in favor of `-open API` flag.
Diffstat (limited to 'plugins/ssr')
-rw-r--r--plugins/ssr/ssrast.mli1
-rw-r--r--plugins/ssr/ssrbwd.ml1
-rw-r--r--plugins/ssr/ssrbwd.mli1
-rw-r--r--plugins/ssr/ssrcommon.ml1
-rw-r--r--plugins/ssr/ssrcommon.mli1
-rw-r--r--plugins/ssr/ssrelim.ml1
-rw-r--r--plugins/ssr/ssrelim.mli1
-rw-r--r--plugins/ssr/ssrequality.ml1
-rw-r--r--plugins/ssr/ssrequality.mli1
-rw-r--r--plugins/ssr/ssrfwd.ml1
-rw-r--r--plugins/ssr/ssrfwd.mli1
-rw-r--r--plugins/ssr/ssripats.ml1
-rw-r--r--plugins/ssr/ssripats.mli1
-rw-r--r--plugins/ssr/ssrparser.ml41
-rw-r--r--plugins/ssr/ssrparser.mli1
-rw-r--r--plugins/ssr/ssrprinters.ml1
-rw-r--r--plugins/ssr/ssrprinters.mli1
-rw-r--r--plugins/ssr/ssrtacticals.ml1
-rw-r--r--plugins/ssr/ssrtacticals.mli1
-rw-r--r--plugins/ssr/ssrvernac.ml41
-rw-r--r--plugins/ssr/ssrview.ml1
-rw-r--r--plugins/ssr/ssrview.mli1
22 files changed, 0 insertions, 22 deletions
diff --git a/plugins/ssr/ssrast.mli b/plugins/ssr/ssrast.mli
index 94eaa1d6a..cdd4ee645 100644
--- a/plugins/ssr/ssrast.mli
+++ b/plugins/ssr/ssrast.mli
@@ -8,7 +8,6 @@
(* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *)
-open API
open Names
open Ltac_plugin
diff --git a/plugins/ssr/ssrbwd.ml b/plugins/ssr/ssrbwd.ml
index 3988f00ba..cc0e86684 100644
--- a/plugins/ssr/ssrbwd.ml
+++ b/plugins/ssr/ssrbwd.ml
@@ -8,7 +8,6 @@
(* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *)
-open API
open Printer
open Pretyping
open Globnames
diff --git a/plugins/ssr/ssrbwd.mli b/plugins/ssr/ssrbwd.mli
index 20a1263d2..af9f7491a 100644
--- a/plugins/ssr/ssrbwd.mli
+++ b/plugins/ssr/ssrbwd.mli
@@ -8,7 +8,6 @@
(* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *)
-open API
val apply_top_tac : Goal.goal Evd.sigma -> Goal.goal list Evd.sigma
diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml
index 411ce6853..608b778e4 100644
--- a/plugins/ssr/ssrcommon.ml
+++ b/plugins/ssr/ssrcommon.ml
@@ -8,7 +8,6 @@
(* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *)
-open API
open Grammar_API
open Util
open Names
diff --git a/plugins/ssr/ssrcommon.mli b/plugins/ssr/ssrcommon.mli
index f61168576..4b045e989 100644
--- a/plugins/ssr/ssrcommon.mli
+++ b/plugins/ssr/ssrcommon.mli
@@ -8,7 +8,6 @@
(* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *)
-open API
open Tacmach
open Names
open Environ
diff --git a/plugins/ssr/ssrelim.ml b/plugins/ssr/ssrelim.ml
index bd9a05891..832044909 100644
--- a/plugins/ssr/ssrelim.ml
+++ b/plugins/ssr/ssrelim.ml
@@ -8,7 +8,6 @@
(* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *)
-open API
open Util
open Names
open Printer
diff --git a/plugins/ssr/ssrelim.mli b/plugins/ssr/ssrelim.mli
index 825b4758e..66e202b48 100644
--- a/plugins/ssr/ssrelim.mli
+++ b/plugins/ssr/ssrelim.mli
@@ -8,7 +8,6 @@
(* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *)
-open API
open Ssrmatching_plugin
val ssrelim :
diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml
index b0fe89897..ab6a60f4e 100644
--- a/plugins/ssr/ssrequality.ml
+++ b/plugins/ssr/ssrequality.ml
@@ -8,7 +8,6 @@
(* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *)
-open API
open Ltac_plugin
open Util
open Names
diff --git a/plugins/ssr/ssrequality.mli b/plugins/ssr/ssrequality.mli
index f9ab5d74f..a3366887f 100644
--- a/plugins/ssr/ssrequality.mli
+++ b/plugins/ssr/ssrequality.mli
@@ -8,7 +8,6 @@
(* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *)
-open API
open Ssrmatching_plugin
open Ssrast
diff --git a/plugins/ssr/ssrfwd.ml b/plugins/ssr/ssrfwd.ml
index 660c2e776..8e6329a15 100644
--- a/plugins/ssr/ssrfwd.ml
+++ b/plugins/ssr/ssrfwd.ml
@@ -8,7 +8,6 @@
(* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *)
-open API
open Names
open Tacmach
diff --git a/plugins/ssr/ssrfwd.mli b/plugins/ssr/ssrfwd.mli
index 7f254074c..e5b5b58ff 100644
--- a/plugins/ssr/ssrfwd.mli
+++ b/plugins/ssr/ssrfwd.mli
@@ -8,7 +8,6 @@
(* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *)
-open API
open Names
open Ltac_plugin
diff --git a/plugins/ssr/ssripats.ml b/plugins/ssr/ssripats.ml
index 06bbd749e..023778fdb 100644
--- a/plugins/ssr/ssripats.ml
+++ b/plugins/ssr/ssripats.ml
@@ -8,7 +8,6 @@
(* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *)
-open API
open Names
open Pp
open Term
diff --git a/plugins/ssr/ssripats.mli b/plugins/ssr/ssripats.mli
index aefdc8e11..6c36e67e8 100644
--- a/plugins/ssr/ssripats.mli
+++ b/plugins/ssr/ssripats.mli
@@ -8,7 +8,6 @@
(* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *)
-open API
open Ssrmatching_plugin
open Ssrast
open Ssrcommon
diff --git a/plugins/ssr/ssrparser.ml4 b/plugins/ssr/ssrparser.ml4
index 09917339a..228444b82 100644
--- a/plugins/ssr/ssrparser.ml4
+++ b/plugins/ssr/ssrparser.ml4
@@ -8,7 +8,6 @@
(* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *)
-open API
open Grammar_API
open Names
open Pp
diff --git a/plugins/ssr/ssrparser.mli b/plugins/ssr/ssrparser.mli
index 154820666..c93e10405 100644
--- a/plugins/ssr/ssrparser.mli
+++ b/plugins/ssr/ssrparser.mli
@@ -8,7 +8,6 @@
(* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *)
-open API
open Grammar_API
val ssrtacarg : Tacexpr.raw_tactic_expr Pcoq.Gram.entry
diff --git a/plugins/ssr/ssrprinters.ml b/plugins/ssr/ssrprinters.ml
index 427109c1b..e865ef706 100644
--- a/plugins/ssr/ssrprinters.ml
+++ b/plugins/ssr/ssrprinters.ml
@@ -8,7 +8,6 @@
(* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *)
-open API
open Pp
open Names
open Printer
diff --git a/plugins/ssr/ssrprinters.mli b/plugins/ssr/ssrprinters.mli
index 8da9bc72b..5c68872b7 100644
--- a/plugins/ssr/ssrprinters.mli
+++ b/plugins/ssr/ssrprinters.mli
@@ -8,7 +8,6 @@
(* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *)
-open API
open Ssrast
val pp_term :
diff --git a/plugins/ssr/ssrtacticals.ml b/plugins/ssr/ssrtacticals.ml
index b586d05e1..5e43c8374 100644
--- a/plugins/ssr/ssrtacticals.ml
+++ b/plugins/ssr/ssrtacticals.ml
@@ -8,7 +8,6 @@
(* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *)
-open API
open Names
open Termops
open Tacmach
diff --git a/plugins/ssr/ssrtacticals.mli b/plugins/ssr/ssrtacticals.mli
index 297cfdfdc..c1f65a31e 100644
--- a/plugins/ssr/ssrtacticals.mli
+++ b/plugins/ssr/ssrtacticals.mli
@@ -8,7 +8,6 @@
(* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *)
-open API
val tclSEQAT :
Ltac_plugin.Tacinterp.interp_sign ->
diff --git a/plugins/ssr/ssrvernac.ml4 b/plugins/ssr/ssrvernac.ml4
index cb6a2cd69..fbe3cd2b9 100644
--- a/plugins/ssr/ssrvernac.ml4
+++ b/plugins/ssr/ssrvernac.ml4
@@ -8,7 +8,6 @@
(* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *)
-open API
open Grammar_API
open Names
open Term
diff --git a/plugins/ssr/ssrview.ml b/plugins/ssr/ssrview.ml
index cc142e091..338ecccc2 100644
--- a/plugins/ssr/ssrview.ml
+++ b/plugins/ssr/ssrview.ml
@@ -8,7 +8,6 @@
(* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *)
-open API
open Util
open Names
open Term
diff --git a/plugins/ssr/ssrview.mli b/plugins/ssr/ssrview.mli
index 8a7bd5d6e..6fd906ff4 100644
--- a/plugins/ssr/ssrview.mli
+++ b/plugins/ssr/ssrview.mli
@@ -8,7 +8,6 @@
(* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *)
-open API
open Ssrast
open Ssrcommon
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-03 17:59:43 +0000