diff options
Diffstat (limited to 'plugins/firstorder')
| -rw-r--r-- | plugins/firstorder/formula.ml | 2 | ||||
| -rw-r--r-- | plugins/firstorder/formula.mli | 2 | ||||
| -rw-r--r-- | plugins/firstorder/g_ground.ml4 | 2 | ||||
| -rw-r--r-- | plugins/firstorder/ground.ml | 2 | ||||
| -rw-r--r-- | plugins/firstorder/ground.mli | 2 | ||||
| -rw-r--r-- | plugins/firstorder/instances.ml | 2 | ||||
| -rw-r--r-- | plugins/firstorder/instances.mli | 2 | ||||
| -rw-r--r-- | plugins/firstorder/rules.ml | 2 | ||||
| -rw-r--r-- | plugins/firstorder/rules.mli | 2 | ||||
| -rw-r--r-- | plugins/firstorder/sequent.ml | 2 | ||||
| -rw-r--r-- | plugins/firstorder/sequent.mli | 2 | ||||
| -rw-r--r-- | plugins/firstorder/unify.ml | 2 | ||||
| -rw-r--r-- | plugins/firstorder/unify.mli | 2 |
13 files changed, 0 insertions, 26 deletions
diff --git a/plugins/firstorder/formula.ml b/plugins/firstorder/formula.ml index 45365cb2cd..3a2ca70b67 100644 --- a/plugins/firstorder/formula.ml +++ b/plugins/firstorder/formula.ml @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) - open Hipattern open Names open Term diff --git a/plugins/firstorder/formula.mli b/plugins/firstorder/formula.mli index 2e89ddb061..77bc481a68 100644 --- a/plugins/firstorder/formula.mli +++ b/plugins/firstorder/formula.mli @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) - open Term open Names open Libnames diff --git a/plugins/firstorder/g_ground.ml4 b/plugins/firstorder/g_ground.ml4 index f85616279d..77f15aa07a 100644 --- a/plugins/firstorder/g_ground.ml4 +++ b/plugins/firstorder/g_ground.ml4 @@ -8,8 +8,6 @@ (*i camlp4deps: "parsing/grammar.cma" i*) -(* $Id$ *) - open Formula open Sequent open Ground diff --git a/plugins/firstorder/ground.ml b/plugins/firstorder/ground.ml index 7f4acb8564..1d9b0c79a8 100644 --- a/plugins/firstorder/ground.ml +++ b/plugins/firstorder/ground.ml @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) - open Formula open Sequent open Rules diff --git a/plugins/firstorder/ground.mli b/plugins/firstorder/ground.mli index 3c0e903fdc..6722a79353 100644 --- a/plugins/firstorder/ground.mli +++ b/plugins/firstorder/ground.mli @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) - val ground_tac: Tacmach.tactic -> (Proof_type.goal Tacmach.sigma -> Sequent.t) -> Tacmach.tactic diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml index 810262a699..b473e5946e 100644 --- a/plugins/firstorder/instances.ml +++ b/plugins/firstorder/instances.ml @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - open Formula open Sequent open Unify diff --git a/plugins/firstorder/instances.mli b/plugins/firstorder/instances.mli index 95dd22ea89..43a1b746c2 100644 --- a/plugins/firstorder/instances.mli +++ b/plugins/firstorder/instances.mli @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - open Term open Tacmach open Names diff --git a/plugins/firstorder/rules.ml b/plugins/firstorder/rules.ml index 515efea701..fcc0f069b1 100644 --- a/plugins/firstorder/rules.ml +++ b/plugins/firstorder/rules.ml @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) - open Util open Names open Term diff --git a/plugins/firstorder/rules.mli b/plugins/firstorder/rules.mli index fc32621ca7..c5498fe0a1 100644 --- a/plugins/firstorder/rules.mli +++ b/plugins/firstorder/rules.mli @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) - open Term open Tacmach open Names diff --git a/plugins/firstorder/sequent.ml b/plugins/firstorder/sequent.ml index 685d44a84d..2f924198c2 100644 --- a/plugins/firstorder/sequent.ml +++ b/plugins/firstorder/sequent.ml @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) - open Term open Util open Formula diff --git a/plugins/firstorder/sequent.mli b/plugins/firstorder/sequent.mli index ce0eddccc2..5e9f46aa28 100644 --- a/plugins/firstorder/sequent.mli +++ b/plugins/firstorder/sequent.mli @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) - open Term open Util open Formula diff --git a/plugins/firstorder/unify.ml b/plugins/firstorder/unify.ml index e3a4c6a559..880e9a7d6d 100644 --- a/plugins/firstorder/unify.ml +++ b/plugins/firstorder/unify.ml @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - open Util open Formula open Tacmach diff --git a/plugins/firstorder/unify.mli b/plugins/firstorder/unify.mli index d6cb3a082d..60abdcd1a0 100644 --- a/plugins/firstorder/unify.mli +++ b/plugins/firstorder/unify.mli @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) - open Term exception UFAIL of constr*constr |