diff options
Diffstat (limited to 'theories/Wellfounded')
| -rw-r--r-- | theories/Wellfounded/Disjoint_Union.v | 2 | ||||
| -rw-r--r-- | theories/Wellfounded/Inclusion.v | 2 | ||||
| -rw-r--r-- | theories/Wellfounded/Inverse_Image.v | 2 | ||||
| -rw-r--r-- | theories/Wellfounded/Lexicographic_Exponentiation.v | 2 | ||||
| -rw-r--r-- | theories/Wellfounded/Lexicographic_Product.v | 2 | ||||
| -rw-r--r-- | theories/Wellfounded/Transitive_Closure.v | 2 | ||||
| -rw-r--r-- | theories/Wellfounded/Union.v | 2 | ||||
| -rw-r--r-- | theories/Wellfounded/Well_Ordering.v | 2 | ||||
| -rw-r--r-- | theories/Wellfounded/Wellfounded.v | 2 |
9 files changed, 0 insertions, 18 deletions
diff --git a/theories/Wellfounded/Disjoint_Union.v b/theories/Wellfounded/Disjoint_Union.v index 785d623b4..f856c8624 100644 --- a/theories/Wellfounded/Disjoint_Union.v +++ b/theories/Wellfounded/Disjoint_Union.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - (** Author: Cristina Cornes From : Constructing Recursion Operators in Type Theory L. Paulson JSC (1986) 2, 325-355 *) diff --git a/theories/Wellfounded/Inclusion.v b/theories/Wellfounded/Inclusion.v index 01049989e..4d7139a51 100644 --- a/theories/Wellfounded/Inclusion.v +++ b/theories/Wellfounded/Inclusion.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - (** Author: Bruno Barras *) Require Import Relation_Definitions. diff --git a/theories/Wellfounded/Inverse_Image.v b/theories/Wellfounded/Inverse_Image.v index c57e70725..6f7a310d5 100644 --- a/theories/Wellfounded/Inverse_Image.v +++ b/theories/Wellfounded/Inverse_Image.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - (** Author: Bruno Barras *) Section Inverse_Image. diff --git a/theories/Wellfounded/Lexicographic_Exponentiation.v b/theories/Wellfounded/Lexicographic_Exponentiation.v index ff1889000..378b47184 100644 --- a/theories/Wellfounded/Lexicographic_Exponentiation.v +++ b/theories/Wellfounded/Lexicographic_Exponentiation.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - (** Author: Cristina Cornes From : Constructing Recursion Operators in Type Theory diff --git a/theories/Wellfounded/Lexicographic_Product.v b/theories/Wellfounded/Lexicographic_Product.v index 5144c0bee..e52c3acae 100644 --- a/theories/Wellfounded/Lexicographic_Product.v +++ b/theories/Wellfounded/Lexicographic_Product.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - (** Authors: Bruno Barras, Cristina Cornes *) Require Import Eqdep. diff --git a/theories/Wellfounded/Transitive_Closure.v b/theories/Wellfounded/Transitive_Closure.v index c999b58ee..a6092fe37 100644 --- a/theories/Wellfounded/Transitive_Closure.v +++ b/theories/Wellfounded/Transitive_Closure.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - (** Author: Bruno Barras *) Require Import Relation_Definitions. diff --git a/theories/Wellfounded/Union.v b/theories/Wellfounded/Union.v index fbb3d9e3c..dbc36e3b1 100644 --- a/theories/Wellfounded/Union.v +++ b/theories/Wellfounded/Union.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - (** Author: Bruno Barras *) Require Import Relation_Operators. diff --git a/theories/Wellfounded/Well_Ordering.v b/theories/Wellfounded/Well_Ordering.v index e11b89248..8a5bf57f0 100644 --- a/theories/Wellfounded/Well_Ordering.v +++ b/theories/Wellfounded/Well_Ordering.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - (** Author: Cristina Cornes. From: Constructing Recursion Operators in Type Theory L. Paulson JSC (1986) 2, 325-355 *) diff --git a/theories/Wellfounded/Wellfounded.v b/theories/Wellfounded/Wellfounded.v index fe05d61ed..77c676fc6 100644 --- a/theories/Wellfounded/Wellfounded.v +++ b/theories/Wellfounded/Wellfounded.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - Require Export Disjoint_Union. Require Export Inclusion. Require Export Inverse_Image. |