diff options
Diffstat (limited to 'theories/Bool')
-rw-r--r-- | theories/Bool/Bool.v | 2 | ||||
-rw-r--r-- | theories/Bool/BoolEq.v | 1 | ||||
-rw-r--r-- | theories/Bool/Bvector.v | 2 | ||||
-rw-r--r-- | theories/Bool/DecBool.v | 2 | ||||
-rw-r--r-- | theories/Bool/IfProp.v | 2 | ||||
-rw-r--r-- | theories/Bool/Sumbool.v | 2 | ||||
-rw-r--r-- | theories/Bool/Zerob.v | 2 |
7 files changed, 0 insertions, 13 deletions
diff --git a/theories/Bool/Bool.v b/theories/Bool/Bool.v index 66ab6f1c8..a1ea2ebc8 100644 --- a/theories/Bool/Bool.v +++ b/theories/Bool/Bool.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - (** The type [bool] is defined in the prelude as [Inductive bool : Set := true : bool | false : bool] *) diff --git a/theories/Bool/BoolEq.v b/theories/Bool/BoolEq.v index 625cbd194..9a2e738eb 100644 --- a/theories/Bool/BoolEq.v +++ b/theories/Bool/BoolEq.v @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) (* Cuihtlauac Alvarado - octobre 2000 *) (** Properties of a boolean equality *) diff --git a/theories/Bool/Bvector.v b/theories/Bool/Bvector.v index d9da08672..b41d65c39 100644 --- a/theories/Bool/Bvector.v +++ b/theories/Bool/Bvector.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - (** Bit vectors. Contribution by Jean Duprat (ENS Lyon). *) Require Export Bool Sumbool. diff --git a/theories/Bool/DecBool.v b/theories/Bool/DecBool.v index 90f7ee662..799438d89 100644 --- a/theories/Bool/DecBool.v +++ b/theories/Bool/DecBool.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - Set Implicit Arguments. Definition ifdec (A B:Prop) (C:Type) (H:{A} + {B}) (x y:C) : C := diff --git a/theories/Bool/IfProp.v b/theories/Bool/IfProp.v index c2b5ed793..573916ddc 100644 --- a/theories/Bool/IfProp.v +++ b/theories/Bool/IfProp.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - Require Import Bool. Inductive IfProp (A B:Prop) : bool -> Prop := diff --git a/theories/Bool/Sumbool.v b/theories/Bool/Sumbool.v index 06ab77cfb..a34c49175 100644 --- a/theories/Bool/Sumbool.v +++ b/theories/Bool/Sumbool.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - (** Here are collected some results about the type sumbool (see INIT/Specif.v) [sumbool A B], which is written [{A}+{B}], is the informative disjunction "A or B", where A and B are logical propositions. diff --git a/theories/Bool/Zerob.v b/theories/Bool/Zerob.v index 5e9d4afa6..fde053026 100644 --- a/theories/Bool/Zerob.v +++ b/theories/Bool/Zerob.v @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - Require Import Arith. Require Import Bool. |