diff options
Diffstat (limited to 'plugins/field')
| -rw-r--r-- | plugins/field/LegacyField.v | 2 | ||||
| -rw-r--r-- | plugins/field/LegacyField_Compl.v | 2 | ||||
| -rw-r--r-- | plugins/field/LegacyField_Tactic.v | 2 | ||||
| -rw-r--r-- | plugins/field/LegacyField_Theory.v | 2 | ||||
| -rw-r--r-- | plugins/field/field.ml4 | 2 |
5 files changed, 0 insertions, 10 deletions
diff --git a/plugins/field/LegacyField.v b/plugins/field/LegacyField.v index efa53b4e9d..bbc1e20b01 100644 --- a/plugins/field/LegacyField.v +++ b/plugins/field/LegacyField.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) - Require Export LegacyField_Compl. Require Export LegacyField_Theory. Require Export LegacyField_Tactic. diff --git a/plugins/field/LegacyField_Compl.v b/plugins/field/LegacyField_Compl.v index d4a39296a0..1df77ef095 100644 --- a/plugins/field/LegacyField_Compl.v +++ b/plugins/field/LegacyField_Compl.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) - Require Import List. Definition assoc_2nd := diff --git a/plugins/field/LegacyField_Tactic.v b/plugins/field/LegacyField_Tactic.v index 5c1f228ac6..50305d4a38 100644 --- a/plugins/field/LegacyField_Tactic.v +++ b/plugins/field/LegacyField_Tactic.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) - Require Import List. Require Import LegacyRing. Require Export LegacyField_Compl. diff --git a/plugins/field/LegacyField_Theory.v b/plugins/field/LegacyField_Theory.v index cc8b043fce..907b137a3e 100644 --- a/plugins/field/LegacyField_Theory.v +++ b/plugins/field/LegacyField_Theory.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) - Require Import List. Require Import Peano_dec. Require Import LegacyRing. diff --git a/plugins/field/field.ml4 b/plugins/field/field.ml4 index 91c0ca21ec..f08ed7db61 100644 --- a/plugins/field/field.ml4 +++ b/plugins/field/field.ml4 @@ -8,8 +8,6 @@ (*i camlp4deps: "parsing/grammar.cma" i*) -(* $Id$ *) - open Names open Pp open Proof_type |
