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/firstorder/formula.ml | 1 - plugins/firstorder/formula.mli | 1 - plugins/firstorder/g_ground.ml4 | 1 - plugins/firstorder/ground.ml | 1 - plugins/firstorder/ground.mli | 1 - plugins/firstorder/instances.ml | 1 - plugins/firstorder/instances.mli | 1 - plugins/firstorder/rules.ml | 1 - plugins/firstorder/rules.mli | 1 - plugins/firstorder/sequent.ml | 1 - plugins/firstorder/sequent.mli | 1 - plugins/firstorder/unify.ml | 1 - plugins/firstorder/unify.mli | 1 - 13 files changed, 13 deletions(-) (limited to 'plugins/firstorder') diff --git a/plugins/firstorder/formula.ml b/plugins/firstorder/formula.ml index 4319fa71c..db1a46a03 100644 --- a/plugins/firstorder/formula.ml +++ b/plugins/firstorder/formula.ml @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open API open Hipattern open Names open Term diff --git a/plugins/firstorder/formula.mli b/plugins/firstorder/formula.mli index 535d75735..106c469c6 100644 --- a/plugins/firstorder/formula.mli +++ b/plugins/firstorder/formula.mli @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open API open Term open EConstr open Globnames diff --git a/plugins/firstorder/g_ground.ml4 b/plugins/firstorder/g_ground.ml4 index 81d714aa2..c001ee382 100644 --- a/plugins/firstorder/g_ground.ml4 +++ b/plugins/firstorder/g_ground.ml4 @@ -8,7 +8,6 @@ (*i camlp4deps: "grammar/grammar.cma" i*) -open API open Grammar_API open Ltac_plugin open Formula diff --git a/plugins/firstorder/ground.ml b/plugins/firstorder/ground.ml index bd420546f..f660ba734 100644 --- a/plugins/firstorder/ground.ml +++ b/plugins/firstorder/ground.ml @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open API open Ltac_plugin open Formula open Sequent diff --git a/plugins/firstorder/ground.mli b/plugins/firstorder/ground.mli index e15af1f23..d763fe635 100644 --- a/plugins/firstorder/ground.mli +++ b/plugins/firstorder/ground.mli @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open API val ground_tac: unit Proofview.tactic -> ((Sequent.t -> unit Proofview.tactic) -> unit Proofview.tactic) -> unit Proofview.tactic diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml index 4c8b96be1..169073630 100644 --- a/plugins/firstorder/instances.ml +++ b/plugins/firstorder/instances.ml @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open API open Unify open Rules open CErrors diff --git a/plugins/firstorder/instances.mli b/plugins/firstorder/instances.mli index c2eb1d68c..ec2a056e3 100644 --- a/plugins/firstorder/instances.mli +++ b/plugins/firstorder/instances.mli @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open API open Globnames open Rules diff --git a/plugins/firstorder/rules.ml b/plugins/firstorder/rules.ml index b0fcd98cc..d6309b057 100644 --- a/plugins/firstorder/rules.ml +++ b/plugins/firstorder/rules.ml @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open API open CErrors open Util open Names diff --git a/plugins/firstorder/rules.mli b/plugins/firstorder/rules.mli index 05f60eccc..d8d4c1a38 100644 --- a/plugins/firstorder/rules.mli +++ b/plugins/firstorder/rules.mli @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open API open Term open EConstr open Names diff --git a/plugins/firstorder/sequent.ml b/plugins/firstorder/sequent.ml index 6fddaafa3..5ba98fb58 100644 --- a/plugins/firstorder/sequent.ml +++ b/plugins/firstorder/sequent.ml @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open API open EConstr open CErrors open Util diff --git a/plugins/firstorder/sequent.mli b/plugins/firstorder/sequent.mli index 2488ffded..0a2e84bb8 100644 --- a/plugins/firstorder/sequent.mli +++ b/plugins/firstorder/sequent.mli @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open API open EConstr open Formula open Globnames diff --git a/plugins/firstorder/unify.ml b/plugins/firstorder/unify.ml index 2da3dc768..a1409edd0 100644 --- a/plugins/firstorder/unify.ml +++ b/plugins/firstorder/unify.ml @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open API open Util open Term open EConstr diff --git a/plugins/firstorder/unify.mli b/plugins/firstorder/unify.mli index cf2ef8ba6..d3e8aeee8 100644 --- a/plugins/firstorder/unify.mli +++ b/plugins/firstorder/unify.mli @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open API open Term open EConstr -- cgit v1.2.3