diff options
| author |  Stephane Glondu <steph@glondu.net> | 2010-08-06 16:15:08 -0400 |
|---|---|---|
| committer | Stephane Glondu <steph@glondu.net> | 2010-08-06 16:17:55 -0400 |
| commit | f18e6146f4fd6ed5b8ded10a3e602f5f64f919f4 (patch) | |
| tree | c413c5bb42d20daf5307634ae6402526bb994fd6 /theories | |
| parent | b9f47391f7f259c24119d1de0a87839e2cc5e80c (diff) | |
Imported Upstream version 8.3~rc1+dfsgupstream/8.3.rc1.dfsg
Diffstat (limited to 'theories')
315 files changed, 383 insertions, 344 deletions
diff --git a/theories/Arith/Arith.v b/theories/Arith/Arith.v index 3cf607d9..0f5ef9d0 100644 --- a/theories/Arith/Arith.v +++ b/theories/Arith/Arith.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: Arith.v 13323 2010-07-24 15:57:30Z herbelin $ i*) Require Export Arith_base. Require Export ArithRing. diff --git a/theories/Arith/Arith_base.v b/theories/Arith/Arith_base.v index e975f273..c5135f63 100644 --- a/theories/Arith/Arith_base.v +++ b/theories/Arith/Arith_base.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: Arith_base.v 13323 2010-07-24 15:57:30Z herbelin $ i*) Require Export Le. Require Export Lt. diff --git a/theories/Arith/Between.v b/theories/Arith/Between.v index 8ab49f25..2ccf802d 100644 --- a/theories/Arith/Between.v +++ b/theories/Arith/Between.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: Between.v 13323 2010-07-24 15:57:30Z herbelin $ i*) Require Import Le. Require Import Lt. diff --git a/theories/Arith/Bool_nat.v b/theories/Arith/Bool_nat.v index 5904e989..9ace38b1 100644 --- a/theories/Arith/Bool_nat.v +++ b/theories/Arith/Bool_nat.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) +(* $Id: Bool_nat.v 13323 2010-07-24 15:57:30Z herbelin $ *) Require Export Compare_dec. Require Export Peano_dec. diff --git a/theories/Arith/Compare.v b/theories/Arith/Compare.v index cdba76eb..2775d132 100644 --- a/theories/Arith/Compare.v +++ b/theories/Arith/Compare.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: Compare.v 13323 2010-07-24 15:57:30Z herbelin $ i*) (** Equality is decidable on [nat] *) diff --git a/theories/Arith/Compare_dec.v b/theories/Arith/Compare_dec.v index 5d20261c..0811fea7 100644 --- a/theories/Arith/Compare_dec.v +++ b/theories/Arith/Compare_dec.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: Compare_dec.v 13323 2010-07-24 15:57:30Z herbelin $ i*) Require Import Le. Require Import Lt. diff --git a/theories/Arith/Div2.v b/theories/Arith/Div2.v index 0a3b7dcc..adbca442 100644 --- a/theories/Arith/Div2.v +++ b/theories/Arith/Div2.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: Div2.v 13323 2010-07-24 15:57:30Z herbelin $ i*) Require Import Lt. Require Import Plus. diff --git a/theories/Arith/EqNat.v b/theories/Arith/EqNat.v index edf31c62..e49e5d14 100644 --- a/theories/Arith/EqNat.v +++ b/theories/Arith/EqNat.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: EqNat.v 13323 2010-07-24 15:57:30Z herbelin $ i*) (** Equality on natural numbers *) diff --git a/theories/Arith/Euclid.v b/theories/Arith/Euclid.v index 78185715..54f4f013 100644 --- a/theories/Arith/Euclid.v +++ b/theories/Arith/Euclid.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: Euclid.v 13323 2010-07-24 15:57:30Z herbelin $ i*) Require Import Mult. Require Import Compare_dec. diff --git a/theories/Arith/Even.v b/theories/Arith/Even.v index 266d51fc..527ad748 100644 --- a/theories/Arith/Even.v +++ b/theories/Arith/Even.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: Even.v 13323 2010-07-24 15:57:30Z herbelin $ i*) (** Here we define the predicates [even] and [odd] by mutual induction and we prove the decidability and the exclusion of those predicates. diff --git a/theories/Arith/Factorial.v b/theories/Arith/Factorial.v index aa8bb7bd..5385bf61 100644 --- a/theories/Arith/Factorial.v +++ b/theories/Arith/Factorial.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: Factorial.v 13323 2010-07-24 15:57:30Z herbelin $ i*) Require Import Plus. Require Import Mult. diff --git a/theories/Arith/Gt.v b/theories/Arith/Gt.v index bcf38c02..eda051df 100644 --- a/theories/Arith/Gt.v +++ b/theories/Arith/Gt.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: Gt.v 13323 2010-07-24 15:57:30Z herbelin $ i*) (** Theorems about [gt] in [nat]. [gt] is defined in [Init/Peano.v] as: << diff --git a/theories/Arith/Le.v b/theories/Arith/Le.v index a8b86ab7..f24667d0 100644 --- a/theories/Arith/Le.v +++ b/theories/Arith/Le.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: Le.v 13323 2010-07-24 15:57:30Z herbelin $ i*) (** Order on natural numbers. [le] is defined in [Init/Peano.v] as: << diff --git a/theories/Arith/Lt.v b/theories/Arith/Lt.v index 68ac6e73..0032741e 100644 --- a/theories/Arith/Lt.v +++ b/theories/Arith/Lt.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: Lt.v 13323 2010-07-24 15:57:30Z herbelin $ i*) (** Theorems about [lt] in nat. [lt] is defined in library [Init/Peano.v] as: << diff --git a/theories/Arith/Max.v b/theories/Arith/Max.v index 3a566321..b4c4d7ad 100644 --- a/theories/Arith/Max.v +++ b/theories/Arith/Max.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: Max.v 13323 2010-07-24 15:57:30Z herbelin $ i*) (** THIS FILE IS DEPRECATED. Use [MinMax] instead. *) diff --git a/theories/Arith/Min.v b/theories/Arith/Min.v index f646c80a..81142249 100644 --- a/theories/Arith/Min.v +++ b/theories/Arith/Min.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: Min.v 13323 2010-07-24 15:57:30Z herbelin $ i*) (** THIS FILE IS DEPRECATED. Use [MinMax] instead. *) diff --git a/theories/Arith/Minus.v b/theories/Arith/Minus.v index 74d2c9a8..39062348 100644 --- a/theories/Arith/Minus.v +++ b/theories/Arith/Minus.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: Minus.v 13323 2010-07-24 15:57:30Z herbelin $ i*) (** [minus] (difference between two natural numbers) is defined in [Init/Peano.v] as: << diff --git a/theories/Arith/Mult.v b/theories/Arith/Mult.v index bfefb967..3ba98472 100644 --- a/theories/Arith/Mult.v +++ b/theories/Arith/Mult.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: Mult.v 13323 2010-07-24 15:57:30Z herbelin $ i*) Require Export Plus. Require Export Minus. diff --git a/theories/Arith/Peano_dec.v b/theories/Arith/Peano_dec.v index 5eb86168..908f99f0 100644 --- a/theories/Arith/Peano_dec.v +++ b/theories/Arith/Peano_dec.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: Peano_dec.v 13323 2010-07-24 15:57:30Z herbelin $ i*) Require Import Decidable. diff --git a/theories/Arith/Plus.v b/theories/Arith/Plus.v index 2ea65696..3c5f28b6 100644 --- a/theories/Arith/Plus.v +++ b/theories/Arith/Plus.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: Plus.v 13323 2010-07-24 15:57:30Z herbelin $ i*) (** Properties of addition. [add] is defined in [Init/Peano.v] as: << diff --git a/theories/Arith/Wf_nat.v b/theories/Arith/Wf_nat.v index a42c38eb..07ab1c3e 100644 --- a/theories/Arith/Wf_nat.v +++ b/theories/Arith/Wf_nat.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: Wf_nat.v 13323 2010-07-24 15:57:30Z herbelin $ i*) (** Well-founded relations and natural numbers *) diff --git a/theories/Bool/Bool.v b/theories/Bool/Bool.v index 43ffde86..8f3c29c6 100644 --- a/theories/Bool/Bool.v +++ b/theories/Bool/Bool.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: Bool.v 13323 2010-07-24 15:57:30Z herbelin $ 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 2c3952e7..9a006e80 100644 --- a/theories/Bool/BoolEq.v +++ b/theories/Bool/BoolEq.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: BoolEq.v 13323 2010-07-24 15:57:30Z herbelin $ i*) (* Cuihtlauac Alvarado - octobre 2000 *) (** Properties of a boolean equality *) diff --git a/theories/Bool/Bvector.v b/theories/Bool/Bvector.v index 5190a246..3f3acccf 100644 --- a/theories/Bool/Bvector.v +++ b/theories/Bool/Bvector.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: Bvector.v 13323 2010-07-24 15:57:30Z herbelin $ i*) (** Bit vectors. Contribution by Jean Duprat (ENS Lyon). *) diff --git a/theories/Bool/DecBool.v b/theories/Bool/DecBool.v index 746507c4..f3123a7a 100644 --- a/theories/Bool/DecBool.v +++ b/theories/Bool/DecBool.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: DecBool.v 13323 2010-07-24 15:57:30Z herbelin $ i*) Set Implicit Arguments. diff --git a/theories/Bool/IfProp.v b/theories/Bool/IfProp.v index 2d0f15a1..dcab1446 100644 --- a/theories/Bool/IfProp.v +++ b/theories/Bool/IfProp.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: IfProp.v 13323 2010-07-24 15:57:30Z herbelin $ i*) Require Import Bool. diff --git a/theories/Bool/Sumbool.v b/theories/Bool/Sumbool.v index 7945fbae..543ff67d 100644 --- a/theories/Bool/Sumbool.v +++ b/theories/Bool/Sumbool.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: Sumbool.v 13323 2010-07-24 15:57:30Z herbelin $ 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 diff --git a/theories/Bool/Zerob.v b/theories/Bool/Zerob.v index 1c6b84ce..a89138d1 100644 --- a/theories/Bool/Zerob.v +++ b/theories/Bool/Zerob.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: Zerob.v 13323 2010-07-24 15:57:30Z herbelin $ i*) Require Import Arith. Require Import Bool. diff --git a/theories/Classes/EquivDec.v b/theories/Classes/EquivDec.v index 5748a5f3..cc6e8936 100644 --- a/theories/Classes/EquivDec.v +++ b/theories/Classes/EquivDec.v @@ -12,7 +12,7 @@ Institution: LRI, CNRS UMR 8623 - University Paris Sud *) -(* $Id$ *) +(* $Id: EquivDec.v 13323 2010-07-24 15:57:30Z herbelin $ *) (** Export notations. *) diff --git a/theories/Classes/Equivalence.v b/theories/Classes/Equivalence.v index 65231ce1..3d8c3434 100644 --- a/theories/Classes/Equivalence.v +++ b/theories/Classes/Equivalence.v @@ -12,7 +12,7 @@ Institution: LRI, CNRS UMR 8623 - University Paris Sud *) -(* $Id$ *) +(* $Id: Equivalence.v 13323 2010-07-24 15:57:30Z herbelin $ *) Require Import Coq.Program.Basics. Require Import Coq.Program.Tactics. diff --git a/theories/Classes/Init.v b/theories/Classes/Init.v index 6e576c96..8cc1216b 100644 --- a/theories/Classes/Init.v +++ b/theories/Classes/Init.v @@ -13,7 +13,7 @@ Institution: LRI, CNRS UMR 8623 - University Paris Sud *) -(* $Id$ *) +(* $Id: Init.v 13323 2010-07-24 15:57:30Z herbelin $ *) (** Hints for the proof search: these combinators should be considered rigid. *) diff --git a/theories/Classes/Morphisms.v b/theories/Classes/Morphisms.v index 9895c5a4..d31829e1 100644 --- a/theories/Classes/Morphisms.v +++ b/theories/Classes/Morphisms.v @@ -13,7 +13,7 @@ Institution: LRI, CNRS UMR 8623 - University Paris Sud *) -(* $Id$ *) +(* $Id: Morphisms.v 13359 2010-07-30 08:46:55Z herbelin $ *) Require Import Coq.Program.Basics. Require Import Coq.Program.Tactics. @@ -23,6 +23,12 @@ Require Export Coq.Classes.RelationClasses. Generalizable All Variables. Local Obligation Tactic := simpl_relation. +Local Notation "'λ' x .. y , t" := (fun x => .. (fun y => t) ..) + (at level 200, x binder, y binder, right associativity). + +Local Notation "'Π' x .. y , P" := (forall x, .. (forall y, P) ..) + (at level 200, x binder, y binder, right associativity) : type_scope. + (** * Morphisms. We now turn to the definition of [Proper] and declare standard instances. diff --git a/theories/Classes/RelationClasses.v b/theories/Classes/RelationClasses.v index 89c23b3e..1aad3cec 100644 --- a/theories/Classes/RelationClasses.v +++ b/theories/Classes/RelationClasses.v @@ -15,7 +15,7 @@ Institution: LRI, CNRS UMR 8623 - University Paris Sud *) -(* $Id$ *) +(* $Id: RelationClasses.v 13344 2010-07-28 15:04:36Z msozeau $ *) Require Export Coq.Classes.Init. Require Import Coq.Program.Basics. @@ -76,7 +76,7 @@ Hint Extern 4 => solve_relation : relations. Generalizable Variables A B C D R S T U l eqA eqB eqC eqD. -Program Lemma flip_Reflexive `(Reflexive A R) : Reflexive (flip R). +Lemma flip_Reflexive `{Reflexive A R} : Reflexive (flip R). Proof. tauto. Qed. Hint Extern 3 (Reflexive (flip _)) => apply flip_Reflexive : typeclass_instances. diff --git a/theories/Classes/SetoidClass.v b/theories/Classes/SetoidClass.v index ff91bd91..b20f9d88 100644 --- a/theories/Classes/SetoidClass.v +++ b/theories/Classes/SetoidClass.v @@ -12,7 +12,7 @@ Institution: LRI, CNRS UMR 8623 - University Paris Sud *) -(* $Id$ *) +(* $Id: SetoidClass.v 13323 2010-07-24 15:57:30Z herbelin $ *) Set Implicit Arguments. Unset Strict Implicit. diff --git a/theories/Classes/SetoidDec.v b/theories/Classes/SetoidDec.v index 6e92a5de..fe775abb 100644 --- a/theories/Classes/SetoidDec.v +++ b/theories/Classes/SetoidDec.v @@ -13,13 +13,16 @@ Institution: LRI, CNRS UMR 8623 - University Paris Sud *) -(* $Id$ *) +(* $Id: SetoidDec.v 13359 2010-07-30 08:46:55Z herbelin $ *) Set Implicit Arguments. Unset Strict Implicit. Generalizable Variables A B . +Local Notation "'λ' x .. y , t" := (fun x => .. (fun y => t) ..) + (at level 200, x binder, y binder, right associativity). + (** Export notations. *) Require Export Coq.Classes.SetoidClass. diff --git a/theories/Classes/SetoidTactics.v b/theories/Classes/SetoidTactics.v index fd3b9f3b..0d43de5a 100644 --- a/theories/Classes/SetoidTactics.v +++ b/theories/Classes/SetoidTactics.v @@ -12,7 +12,7 @@ Institution: LRI, CNRS UMR 8623 - University Paris Sud *) -(* $Id$ *) +(* $Id: SetoidTactics.v 13323 2010-07-24 15:57:30Z herbelin $ *) Require Import Coq.Classes.Morphisms Coq.Classes.Morphisms_Prop. Require Export Coq.Classes.RelationClasses Coq.Relations.Relation_Definitions. diff --git a/theories/FSets/FMapAVL.v b/theories/FSets/FMapAVL.v index 8158324e..7b64ded7 100644 --- a/theories/FSets/FMapAVL.v +++ b/theories/FSets/FMapAVL.v @@ -8,7 +8,7 @@ (* Finite map library. *) -(* $Id$ *) +(* $Id: FMapAVL.v 13090 2010-06-08 13:56:14Z herbelin $ *) (** * FMapAVL *) diff --git a/theories/FSets/FMapFacts.v b/theories/FSets/FMapFacts.v index 4c59971c..8944f7ce 100644 --- a/theories/FSets/FMapFacts.v +++ b/theories/FSets/FMapFacts.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -(* $Id$ *) +(* $Id: FMapFacts.v 12459 2009-11-02 18:51:43Z letouzey $ *) (** * Finite maps library *) diff --git a/theories/FSets/FMapFullAVL.v b/theories/FSets/FMapFullAVL.v index e4f8b4df..2b9e7077 100644 --- a/theories/FSets/FMapFullAVL.v +++ b/theories/FSets/FMapFullAVL.v @@ -8,7 +8,7 @@ (* Finite map library. *) -(* $Id$ *) +(* $Id: FMapFullAVL.v 13090 2010-06-08 13:56:14Z herbelin $ *) (** * FMapFullAVL diff --git a/theories/FSets/FMapInterface.v b/theories/FSets/FMapInterface.v index e60cca9d..bbfecfb1 100644 --- a/theories/FSets/FMapInterface.v +++ b/theories/FSets/FMapInterface.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -(* $Id$ *) +(* $Id: FMapInterface.v 12640 2010-01-07 15:32:49Z letouzey $ *) (** * Finite map library *) diff --git a/theories/FSets/FMapList.v b/theories/FSets/FMapList.v index 56fc35d8..4b7f183c 100644 --- a/theories/FSets/FMapList.v +++ b/theories/FSets/FMapList.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -(* $Id$ *) +(* $Id: FMapList.v 12458 2009-11-02 18:50:33Z letouzey $ *) (** * Finite map library *) diff --git a/theories/FSets/FMapPositive.v b/theories/FSets/FMapPositive.v index 7c5a4fa1..30bce2db 100644 --- a/theories/FSets/FMapPositive.v +++ b/theories/FSets/FMapPositive.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -(* $Id$ *) +(* $Id: FMapPositive.v 13297 2010-07-19 23:32:42Z letouzey $ *) (** * FMapPositive : an implementation of FMapInterface for [positive] keys. *) diff --git a/theories/FSets/FMapWeakList.v b/theories/FSets/FMapWeakList.v index 38ed172b..db479ea8 100644 --- a/theories/FSets/FMapWeakList.v +++ b/theories/FSets/FMapWeakList.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -(* $Id$ *) +(* $Id: FMapWeakList.v 12458 2009-11-02 18:50:33Z letouzey $ *) (** * Finite map library *) diff --git a/theories/FSets/FMaps.v b/theories/FSets/FMaps.v index 6b110240..75904202 100644 --- a/theories/FSets/FMaps.v +++ b/theories/FSets/FMaps.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -(* $Id$ *) +(* $Id: FMaps.v 10699 2008-03-19 20:56:43Z letouzey $ *) Require Export OrderedType OrderedTypeEx OrderedTypeAlt. diff --git a/theories/FSets/FSetAVL.v b/theories/FSets/FSetAVL.v index bc6c731f..2cbba723 100644 --- a/theories/FSets/FSetAVL.v +++ b/theories/FSets/FSetAVL.v @@ -7,7 +7,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -(* $Id$ *) +(* $Id: FSetAVL.v 12641 2010-01-07 15:32:52Z letouzey $ *) (** * FSetAVL : Implementation of FSetInterface via AVL trees *) diff --git a/theories/FSets/FSetBridge.v b/theories/FSets/FSetBridge.v index 7f8c51d6..c2d921be 100644 --- a/theories/FSets/FSetBridge.v +++ b/theories/FSets/FSetBridge.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -(* $Id$ *) +(* $Id: FSetBridge.v 13253 2010-07-07 08:39:30Z letouzey $ *) (** * Finite sets library *) diff --git a/theories/FSets/FSetDecide.v b/theories/FSets/FSetDecide.v index b7d6382e..497f4e6d 100644 --- a/theories/FSets/FSetDecide.v +++ b/theories/FSets/FSetDecide.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -(* $Id$ *) +(* $Id: FSetDecide.v 13171 2010-06-18 21:45:40Z letouzey $ *) (**************************************************************) (* FSetDecide.v *) diff --git a/theories/FSets/FSetEqProperties.v b/theories/FSets/FSetEqProperties.v index ec0c6a55..ac55aef5 100644 --- a/theories/FSets/FSetEqProperties.v +++ b/theories/FSets/FSetEqProperties.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -(* $Id$ *) +(* $Id: FSetEqProperties.v 12400 2009-10-19 13:14:18Z letouzey $ *) (** * Finite sets library *) diff --git a/theories/FSets/FSetFacts.v b/theories/FSets/FSetFacts.v index b750edfc..45b43d83 100644 --- a/theories/FSets/FSetFacts.v +++ b/theories/FSets/FSetFacts.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -(* $Id$ *) +(* $Id: FSetFacts.v 12461 2009-11-03 08:24:06Z letouzey $ *) (** * Finite sets library *) diff --git a/theories/FSets/FSetInterface.v b/theories/FSets/FSetInterface.v index 8aede552..f366ed3e 100644 --- a/theories/FSets/FSetInterface.v +++ b/theories/FSets/FSetInterface.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -(* $Id$ *) +(* $Id: FSetInterface.v 12640 2010-01-07 15:32:49Z letouzey $ *) (** * Finite set library *) diff --git a/theories/FSets/FSetList.v b/theories/FSets/FSetList.v index f83259c4..9408ba05 100644 --- a/theories/FSets/FSetList.v +++ b/theories/FSets/FSetList.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -(* $Id$ *) +(* $Id: FSetList.v 12641 2010-01-07 15:32:52Z letouzey $ *) (** * Finite sets library *) diff --git a/theories/FSets/FSetProperties.v b/theories/FSets/FSetProperties.v index 84c26dac..59e19cd3 100644 --- a/theories/FSets/FSetProperties.v +++ b/theories/FSets/FSetProperties.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -(* $Id$ *) +(* $Id: FSetProperties.v 12400 2009-10-19 13:14:18Z letouzey $ *) (** * Finite sets library *) diff --git a/theories/FSets/FSetToFiniteSet.v b/theories/FSets/FSetToFiniteSet.v index 01138270..2aa1b433 100644 --- a/theories/FSets/FSetToFiniteSet.v +++ b/theories/FSets/FSetToFiniteSet.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -(* $Id$ *) +(* $Id: FSetToFiniteSet.v 12363 2009-09-28 15:04:07Z letouzey $ *) (** * Finite sets library : conversion to old [Finite_sets] *) diff --git a/theories/FSets/FSetWeakList.v b/theories/FSets/FSetWeakList.v index 711cbd9a..b55db37a 100644 --- a/theories/FSets/FSetWeakList.v +++ b/theories/FSets/FSetWeakList.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -(* $Id$ *) +(* $Id: FSetWeakList.v 12641 2010-01-07 15:32:52Z letouzey $ *) (** * Finite sets library *) diff --git a/theories/FSets/FSets.v b/theories/FSets/FSets.v index 62a95734..a725c1eb 100644 --- a/theories/FSets/FSets.v +++ b/theories/FSets/FSets.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -(* $Id$ *) +(* $Id: FSets.v 13297 2010-07-19 23:32:42Z letouzey $ *) Require Export OrderedType. Require Export OrderedTypeEx. diff --git a/theories/Init/Datatypes.v b/theories/Init/Datatypes.v index 62e0d398..7f2ea63d 100644 --- a/theories/Init/Datatypes.v +++ b/theories/Init/Datatypes.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: Datatypes.v 13323 2010-07-24 15:57:30Z herbelin $ i*) Set Implicit Arguments. diff --git a/theories/Init/Logic.v b/theories/Init/Logic.v index 16c32b35..4c9bd919 100644 --- a/theories/Init/Logic.v +++ b/theories/Init/Logic.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: Logic.v 13323 2010-07-24 15:57:30Z herbelin $ i*) Set Implicit Arguments. diff --git a/theories/Init/Logic_Type.v b/theories/Init/Logic_Type.v index d002c967..b9ea3095 100644 --- a/theories/Init/Logic_Type.v +++ b/theories/Init/Logic_Type.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: Logic_Type.v 13323 2010-07-24 15:57:30Z herbelin $ i*) (** This module defines type constructors for types in [Type] ([Datatypes.v] and [Logic.v] defined them for types in [Set]) *) diff --git a/theories/Init/Notations.v b/theories/Init/Notations.v index e8a11952..0eba44b3 100644 --- a/theories/Init/Notations.v +++ b/theories/Init/Notations.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: Notations.v 13323 2010-07-24 15:57:30Z herbelin $ i*) (** These are the notations whose level and associativity are imposed by Coq *) diff --git a/theories/Init/Peano.v b/theories/Init/Peano.v index e86939c8..a6f94752 100644 --- a/theories/Init/Peano.v +++ b/theories/Init/Peano.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: Peano.v 13323 2010-07-24 15:57:30Z herbelin $ i*) (** The type [nat] of Peano natural numbers (built from [O] and [S]) is defined in [Datatypes.v] *) diff --git a/theories/Init/Prelude.v b/theories/Init/Prelude.v index d7625147..63d53560 100644 --- a/theories/Init/Prelude.v +++ b/theories/Init/Prelude.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: Prelude.v 13323 2010-07-24 15:57:30Z herbelin $ i*) Require Export Notations. Require Export Logic. diff --git a/theories/Init/Specif.v b/theories/Init/Specif.v index 26c0194e..436a7957 100644 --- a/theories/Init/Specif.v +++ b/theories/Init/Specif.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: Specif.v 13323 2010-07-24 15:57:30Z herbelin $ i*) (** Basic specifications : sets that may contain logical information *) diff --git a/theories/Init/Tactics.v b/theories/Init/Tactics.v index 3a845e6a..58920228 100644 --- a/theories/Init/Tactics.v +++ b/theories/Init/Tactics.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: Tactics.v 13323 2010-07-24 15:57:30Z herbelin $ i*) Require Import Notations. Require Import Logic. diff --git a/theories/Init/Wf.v b/theories/Init/Wf.v index a7887913..be7becda 100644 --- a/theories/Init/Wf.v +++ b/theories/Init/Wf.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: Wf.v 13323 2010-07-24 15:57:30Z herbelin $ i*) (** * This module proves the validity of - well-founded recursion (also known as course of values) diff --git a/theories/Lists/List.v b/theories/Lists/List.v index bc55ef02..c4957578 100644 --- a/theories/Lists/List.v +++ b/theories/Lists/List.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: List.v 13323 2010-07-24 15:57:30Z herbelin $ i*) Require Import Le Gt Minus Min Bool. diff --git a/theories/Lists/ListSet.v b/theories/Lists/ListSet.v index 9978f5bc..2833ca3e 100644 --- a/theories/Lists/ListSet.v +++ b/theories/Lists/ListSet.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: ListSet.v 13323 2010-07-24 15:57:30Z herbelin $ i*) (** A Library for finite sets, implemented as lists *) diff --git a/theories/Lists/ListTactics.v b/theories/Lists/ListTactics.v index c7d37dd9..5de2780a 100644 --- a/theories/Lists/ListTactics.v +++ b/theories/Lists/ListTactics.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: ListTactics.v 13323 2010-07-24 15:57:30Z herbelin $ i*) Require Import BinPos. Require Import List. diff --git a/theories/Lists/SetoidList.v b/theories/Lists/SetoidList.v index d42e71e5..ec31f37d 100644 --- a/theories/Lists/SetoidList.v +++ b/theories/Lists/SetoidList.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -(* $Id$ *) +(* $Id: SetoidList.v 12919 2010-04-10 16:30:44Z herbelin $ *) Require Export List. Require Export Sorting. diff --git a/theories/Lists/Streams.v b/theories/Lists/Streams.v index feb8c654..e07347a0 100644 --- a/theories/Lists/Streams.v +++ b/theories/Lists/Streams.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: Streams.v 13323 2010-07-24 15:57:30Z herbelin $ i*) Set Implicit Arguments. diff --git a/theories/Lists/TheoryList.v b/theories/Lists/TheoryList.v index bb5c7b17..aa1b099b 100644 --- a/theories/Lists/TheoryList.v +++ b/theories/Lists/TheoryList.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: TheoryList.v 13323 2010-07-24 15:57:30Z herbelin $ i*) (** Some programs and results about lists following CAML Manual *) diff --git a/theories/Logic/Berardi.v b/theories/Logic/Berardi.v index 7d9fb802..c4c8bbe2 100644 --- a/theories/Logic/Berardi.v +++ b/theories/Logic/Berardi.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: Berardi.v 13323 2010-07-24 15:57:30Z herbelin $ i*) (** This file formalizes Berardi's paradox which says that in the calculus of constructions, excluded middle (EM) and axiom of diff --git a/theories/Logic/ChoiceFacts.v b/theories/Logic/ChoiceFacts.v index 959670cb..34ebc329 100644 --- a/theories/Logic/ChoiceFacts.v +++ b/theories/Logic/ChoiceFacts.v @@ -7,7 +7,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: ChoiceFacts.v 12363 2009-09-28 15:04:07Z letouzey $ i*) +(*i $Id: ChoiceFacts.v 13323 2010-07-24 15:57:30Z herbelin $ i*) (** Some facts and definitions concerning choice and description in intuitionistic logic. diff --git a/theories/Logic/Classical.v b/theories/Logic/Classical.v index b2cca5c2..d6c79882 100644 --- a/theories/Logic/Classical.v +++ b/theories/Logic/Classical.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: Classical.v 13323 2010-07-24 15:57:30Z herbelin $ i*) (** Classical Logic *) diff --git a/theories/Logic/ClassicalChoice.v b/theories/Logic/ClassicalChoice.v index 50ce871b..08a34bc8 100644 --- a/theories/Logic/ClassicalChoice.v +++ b/theories/Logic/ClassicalChoice.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: ClassicalChoice.v 13323 2010-07-24 15:57:30Z herbelin $ i*) (** This file provides classical logic and functional choice; this especially provides both indefinite descriptions and choice functions diff --git a/theories/Logic/ClassicalDescription.v b/theories/Logic/ClassicalDescription.v index 793c6ab7..f9896669 100644 --- a/theories/Logic/ClassicalDescription.v +++ b/theories/Logic/ClassicalDescription.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: ClassicalDescription.v 13323 2010-07-24 15:57:30Z herbelin $ i*) (** This file provides classical logic and definite description, which is equivalent to providing classical logic and Church's iota operator *) diff --git a/theories/Logic/ClassicalEpsilon.v b/theories/Logic/ClassicalEpsilon.v index 53989d07..c45bc052 100644 --- a/theories/Logic/ClassicalEpsilon.v +++ b/theories/Logic/ClassicalEpsilon.v @@ -7,7 +7,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: ClassicalEpsilon.v 13323 2010-07-24 15:57:30Z herbelin $ i*) (** This file provides classical logic and indefinite description under the form of Hilbert's epsilon operator *) diff --git a/theories/Logic/ClassicalFacts.v b/theories/Logic/ClassicalFacts.v index c5822bac..cd885592 100644 --- a/theories/Logic/ClassicalFacts.v +++ b/theories/Logic/ClassicalFacts.v @@ -7,7 +7,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: ClassicalFacts.v 13323 2010-07-24 15:57:30Z herbelin $ i*) (** Some facts and definitions about classical logic diff --git a/theories/Logic/ClassicalUniqueChoice.v b/theories/Logic/ClassicalUniqueChoice.v index 6c1c68cf..ea0898d4 100644 --- a/theories/Logic/ClassicalUniqueChoice.v +++ b/theories/Logic/ClassicalUniqueChoice.v @@ -7,7 +7,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: ClassicalUniqueChoice.v 13323 2010-07-24 15:57:30Z herbelin $ i*) (** This file provides classical logic and unique choice; this is weaker than providing iota operator and classical logic as the diff --git a/theories/Logic/Classical_Pred_Set.v b/theories/Logic/Classical_Pred_Set.v index 3f30abe5..b95373e5 100644 --- a/theories/Logic/Classical_Pred_Set.v +++ b/theories/Logic/Classical_Pred_Set.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: Classical_Pred_Set.v 13323 2010-07-24 15:57:30Z herbelin $ i*) (** This file is obsolete, use Classical_Pred_Type.v via Classical.v instead *) diff --git a/theories/Logic/Classical_Pred_Type.v b/theories/Logic/Classical_Pred_Type.v index 638c58d2..32f0a6ac 100644 --- a/theories/Logic/Classical_Pred_Type.v +++ b/theories/Logic/Classical_Pred_Type.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: Classical_Pred_Type.v 13323 2010-07-24 15:57:30Z herbelin $ i*) (** Classical Predicate Logic on Type *) diff --git a/theories/Logic/Classical_Prop.v b/theories/Logic/Classical_Prop.v index 91392ca6..77715ce3 100644 --- a/theories/Logic/Classical_Prop.v +++ b/theories/Logic/Classical_Prop.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: Classical_Prop.v 13323 2010-07-24 15:57:30Z herbelin $ i*) (** Classical Propositional Logic *) diff --git a/theories/Logic/Classical_Type.v b/theories/Logic/Classical_Type.v index 2f5c9726..2319638f 100644 --- a/theories/Logic/Classical_Type.v +++ b/theories/Logic/Classical_Type.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: Classical_Type.v 13323 2010-07-24 15:57:30Z herbelin $ i*) (** This file is obsolete, use Classical.v instead *) diff --git a/theories/Logic/ConstructiveEpsilon.v b/theories/Logic/ConstructiveEpsilon.v index 90aa0f30..738ca1d5 100644 --- a/theories/Logic/ConstructiveEpsilon.v +++ b/theories/Logic/ConstructiveEpsilon.v @@ -6,9 +6,9 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: ConstructiveEpsilon.v 13323 2010-07-24 15:57:30Z herbelin $ i*) -(*i $Id: ConstructiveEpsilon.v 12112 2009-04-28 15:47:34Z herbelin $ i*) +(*i $Id: ConstructiveEpsilon.v 13323 2010-07-24 15:57:30Z herbelin $ i*) (** This module proves the constructive description schema, which infers the sigma-existence (i.e., [Set]-existence) of a witness to a diff --git a/theories/Logic/Decidable.v b/theories/Logic/Decidable.v index df9acbcc..ac4f686b 100644 --- a/theories/Logic/Decidable.v +++ b/theories/Logic/Decidable.v @@ -5,7 +5,7 @@ (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: Decidable.v 13323 2010-07-24 15:57:30Z herbelin $ i*) (** Properties of decidable propositions *) diff --git a/theories/Logic/Description.v b/theories/Logic/Description.v index c569dc46..deedf35b 100644 --- a/theories/Logic/Description.v +++ b/theories/Logic/Description.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: Description.v 13323 2010-07-24 15:57:30Z herbelin $ i*) (** This file provides a constructive form of definite description; it allows to build functions from the proof of their existence in any diff --git a/theories/Logic/Diaconescu.v b/theories/Logic/Diaconescu.v index 4c4785cf..ff640af7 100644 --- a/theories/Logic/Diaconescu.v +++ b/theories/Logic/Diaconescu.v @@ -7,7 +7,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: Diaconescu.v 13323 2010-07-24 15:57:30Z herbelin $ i*) (** Diaconescu showed that the Axiom of Choice entails Excluded-Middle in topoi [Diaconescu75]. Lacas and Werner adapted the proof to show diff --git a/theories/Logic/Epsilon.v b/theories/Logic/Epsilon.v index 9cea8dfd..4ec0c83d 100644 --- a/theories/Logic/Epsilon.v +++ b/theories/Logic/Epsilon.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: Epsilon.v 13323 2010-07-24 15:57:30Z herbelin $ i*) (** This file provides indefinite description under the form of Hilbert's epsilon operator; it does not assume classical logic. *) diff --git a/theories/Logic/Eqdep.v b/theories/Logic/Eqdep.v index ed9d1a9f..53b19ff6 100644 --- a/theories/Logic/Eqdep.v +++ b/theories/Logic/Eqdep.v @@ -7,7 +7,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: Eqdep.v 13332 2010-07-26 22:12:43Z msozeau $ i*) (** This file axiomatizes the invariance by substitution of reflexive equality proofs [[Streicher93]] and exports its consequences, such @@ -31,5 +31,5 @@ Export EqdepTheory. (** Exported hints *) -Hint Resolve eq_dep_eq: core v62. -Hint Resolve inj_pair2 inj_pairT2: core. +Hint Resolve eq_dep_eq: eqdep v62. +Hint Resolve inj_pair2 inj_pairT2: eqdep. diff --git a/theories/Logic/EqdepFacts.v b/theories/Logic/EqdepFacts.v index 15a36dd4..3e49c759 100644 --- a/theories/Logic/EqdepFacts.v +++ b/theories/Logic/EqdepFacts.v @@ -7,7 +7,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: EqdepFacts.v 13323 2010-07-24 15:57:30Z herbelin $ i*) (** This file defines dependent equality and shows its equivalence with equality on dependent pairs (inhabiting sigma-types). It derives diff --git a/theories/Logic/Eqdep_dec.v b/theories/Logic/Eqdep_dec.v index 0ad7e909..c45643e4 100644 --- a/theories/Logic/Eqdep_dec.v +++ b/theories/Logic/Eqdep_dec.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: Eqdep_dec.v 13323 2010-07-24 15:57:30Z herbelin $ i*) (** We prove that there is only one proof of [x=x], i.e [refl_equal x]. This holds if the equality upon the set of [x] is decidable. diff --git a/theories/Logic/FunctionalExtensionality.v b/theories/Logic/FunctionalExtensionality.v index 5e9953d4..4def8910 100644 --- a/theories/Logic/FunctionalExtensionality.v +++ b/theories/Logic/FunctionalExtensionality.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: FunctionalExtensionality.v 13323 2010-07-24 15:57:30Z herbelin $ i*) (** This module states the axiom of (dependent) functional extensionality and (dependent) eta-expansion. It introduces a tactic [extensionality] to apply the axiom of extensionality to an equality goal. *) diff --git a/theories/Logic/IndefiniteDescription.v b/theories/Logic/IndefiniteDescription.v index 05c04952..e0537238 100644 --- a/theories/Logic/IndefiniteDescription.v +++ b/theories/Logic/IndefiniteDescription.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: IndefiniteDescription.v 13323 2010-07-24 15:57:30Z herbelin $ i*) (** This file provides a constructive form of indefinite description that allows to build choice functions; this is weaker than Hilbert's diff --git a/theories/Logic/JMeq.v b/theories/Logic/JMeq.v index 06903c3b..3de77074 100644 --- a/theories/Logic/JMeq.v +++ b/theories/Logic/JMeq.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: JMeq.v 13323 2010-07-24 15:57:30Z herbelin $ i*) (** John Major's Equality as proposed by Conor McBride diff --git a/theories/Logic/RelationalChoice.v b/theories/Logic/RelationalChoice.v index 85da26b3..e0a10d46 100644 --- a/theories/Logic/RelationalChoice.v +++ b/theories/Logic/RelationalChoice.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: RelationalChoice.v 13323 2010-07-24 15:57:30Z herbelin $ i*) (** This file axiomatizes the relational form of the axiom of choice *) diff --git a/theories/NArith/BinNat.v b/theories/NArith/BinNat.v index 332e2104..e44b39f5 100644 --- a/theories/NArith/BinNat.v +++ b/theories/NArith/BinNat.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: BinNat.v 13323 2010-07-24 15:57:30Z herbelin $ i*) Require Import BinPos. Unset Boxed Definitions. diff --git a/theories/NArith/BinPos.v b/theories/NArith/BinPos.v index 9cfb8893..a8f78df0 100644 --- a/theories/NArith/BinPos.v +++ b/theories/NArith/BinPos.v @@ -7,7 +7,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: BinPos.v 13323 2010-07-24 15:57:30Z herbelin $ i*) Unset Boxed Definitions. diff --git a/theories/NArith/NArith.v b/theories/NArith/NArith.v index 9b659750..9d2424bc 100644 --- a/theories/NArith/NArith.v +++ b/theories/NArith/NArith.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) +(* $Id: NArith.v 13323 2010-07-24 15:57:30Z herbelin $ *) (** Library for binary natural numbers *) diff --git a/theories/NArith/Ndec.v b/theories/NArith/Ndec.v index dbea23e3..d6b1e718 100644 --- a/theories/NArith/Ndec.v +++ b/theories/NArith/Ndec.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: Ndec.v 13323 2010-07-24 15:57:30Z herbelin $ i*) Require Import Bool. Require Import Sumbool. diff --git a/theories/NArith/Ndigits.v b/theories/NArith/Ndigits.v index e21f1976..5151236f 100644 --- a/theories/NArith/Ndigits.v +++ b/theories/NArith/Ndigits.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: Ndigits.v 13323 2010-07-24 15:57:30Z herbelin $ i*) Require Import Bool. Require Import Bvector. diff --git a/theories/NArith/Ndist.v b/theories/NArith/Ndist.v index bbf38794..0e920242 100644 --- a/theories/NArith/Ndist.v +++ b/theories/NArith/Ndist.v @@ -5,7 +5,7 @@ (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: Ndist.v 13323 2010-07-24 15:57:30Z herbelin $ i*) Require Import Arith. Require Import Min. diff --git a/theories/NArith/Nnat.v b/theories/NArith/Nnat.v index dec7e927..49bbf7b7 100644 --- a/theories/NArith/Nnat.v +++ b/theories/NArith/Nnat.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: Nnat.v 13323 2010-07-24 15:57:30Z herbelin $ i*) Require Import Arith_base. Require Import Compare_dec. diff --git a/theories/NArith/Pnat.v b/theories/NArith/Pnat.v index 9f995502..1952470d 100644 --- a/theories/NArith/Pnat.v +++ b/theories/NArith/Pnat.v @@ -7,7 +7,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: Pnat.v 13323 2010-07-24 15:57:30Z herbelin $ i*) Require Import BinPos. diff --git a/theories/Numbers/BigNumPrelude.v b/theories/Numbers/BigNumPrelude.v index 356cbb26..97b6b077 100644 --- a/theories/Numbers/BigNumPrelude.v +++ b/theories/Numbers/BigNumPrelude.v @@ -8,7 +8,7 @@ (* Benjamin Gregoire, Laurent Thery, INRIA, 2007 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: BigNumPrelude.v 13323 2010-07-24 15:57:30Z herbelin $ i*) (** * BigNumPrelude *) diff --git a/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v b/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v index 669dc741..29186694 100644 --- a/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v +++ b/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v @@ -8,7 +8,7 @@ (* Benjamin Gregoire, Laurent Thery, INRIA, 2007 *) (************************************************************************) -(* $Id$ *) +(* $Id: CyclicAxioms.v 13323 2010-07-24 15:57:30Z herbelin $ *) (** * Signature and specification of a bounded integer structure *) diff --git a/theories/Numbers/Cyclic/Abstract/NZCyclic.v b/theories/Numbers/Cyclic/Abstract/NZCyclic.v index 3636ebec..e5bc043d 100644 --- a/theories/Numbers/Cyclic/Abstract/NZCyclic.v +++ b/theories/Numbers/Cyclic/Abstract/NZCyclic.v @@ -8,7 +8,7 @@ (* Evgeny Makarov, INRIA, 2007 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: NZCyclic.v 13323 2010-07-24 15:57:30Z herbelin $ i*) Require Export NZAxioms. Require Import BigNumPrelude. diff --git a/theories/Numbers/Cyclic/DoubleCyclic/DoubleAdd.v b/theories/Numbers/Cyclic/DoubleCyclic/DoubleAdd.v index 868b7247..f49201d8 100644 --- a/theories/Numbers/Cyclic/DoubleCyclic/DoubleAdd.v +++ b/theories/Numbers/Cyclic/DoubleCyclic/DoubleAdd.v @@ -8,7 +8,7 @@ (* Benjamin Gregoire, Laurent Thery, INRIA, 2007 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: DoubleAdd.v 13323 2010-07-24 15:57:30Z herbelin $ i*) Set Implicit Arguments. diff --git a/theories/Numbers/Cyclic/DoubleCyclic/DoubleBase.v b/theories/Numbers/Cyclic/DoubleCyclic/DoubleBase.v index a7985c4f..ba2a1770 100644 --- a/theories/Numbers/Cyclic/DoubleCyclic/DoubleBase.v +++ b/theories/Numbers/Cyclic/DoubleCyclic/DoubleBase.v @@ -8,7 +8,7 @@ (* Benjamin Gregoire, Laurent Thery, INRIA, 2007 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: DoubleBase.v 13323 2010-07-24 15:57:30Z herbelin $ i*) Set Implicit Arguments. diff --git a/theories/Numbers/Cyclic/DoubleCyclic/DoubleCyclic.v b/theories/Numbers/Cyclic/DoubleCyclic/DoubleCyclic.v index cbac8723..4a60a10b 100644 --- a/theories/Numbers/Cyclic/DoubleCyclic/DoubleCyclic.v +++ b/theories/Numbers/Cyclic/DoubleCyclic/DoubleCyclic.v @@ -8,7 +8,7 @@ (* Benjamin Gregoire, Laurent Thery, INRIA, 2007 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: DoubleCyclic.v 13323 2010-07-24 15:57:30Z herbelin $ i*) Set Implicit Arguments. diff --git a/theories/Numbers/Cyclic/DoubleCyclic/DoubleDiv.v b/theories/Numbers/Cyclic/DoubleCyclic/DoubleDiv.v index 48750fa7..5ddadd12 100644 --- a/theories/Numbers/Cyclic/DoubleCyclic/DoubleDiv.v +++ b/theories/Numbers/Cyclic/DoubleCyclic/DoubleDiv.v @@ -8,7 +8,7 @@ (* Benjamin Gregoire, Laurent Thery, INRIA, 2007 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: DoubleDiv.v 13323 2010-07-24 15:57:30Z herbelin $ i*) Set Implicit Arguments. diff --git a/theories/Numbers/Cyclic/DoubleCyclic/DoubleDivn1.v b/theories/Numbers/Cyclic/DoubleCyclic/DoubleDivn1.v index f241cc54..3ada7d40 100644 --- a/theories/Numbers/Cyclic/DoubleCyclic/DoubleDivn1.v +++ b/theories/Numbers/Cyclic/DoubleCyclic/DoubleDivn1.v @@ -8,7 +8,7 @@ (* Benjamin Gregoire, Laurent Thery, INRIA, 2007 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: DoubleDivn1.v 13323 2010-07-24 15:57:30Z herbelin $ i*) Set Implicit Arguments. diff --git a/theories/Numbers/Cyclic/DoubleCyclic/DoubleLift.v b/theories/Numbers/Cyclic/DoubleCyclic/DoubleLift.v index 26af1cc8..3989791c 100644 --- a/theories/Numbers/Cyclic/DoubleCyclic/DoubleLift.v +++ b/theories/Numbers/Cyclic/DoubleCyclic/DoubleLift.v @@ -8,7 +8,7 @@ (* Benjamin Gregoire, Laurent Thery, INRIA, 2007 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: DoubleLift.v 13323 2010-07-24 15:57:30Z herbelin $ i*) Set Implicit Arguments. diff --git a/theories/Numbers/Cyclic/DoubleCyclic/DoubleMul.v b/theories/Numbers/Cyclic/DoubleCyclic/DoubleMul.v index fafb7d1d..7ddb0468 100644 --- a/theories/Numbers/Cyclic/DoubleCyclic/DoubleMul.v +++ b/theories/Numbers/Cyclic/DoubleCyclic/DoubleMul.v @@ -8,7 +8,7 @@ (* Benjamin Gregoire, Laurent Thery, INRIA, 2007 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: DoubleMul.v 13323 2010-07-24 15:57:30Z herbelin $ i*) Set Implicit Arguments. diff --git a/theories/Numbers/Cyclic/DoubleCyclic/DoubleSqrt.v b/theories/Numbers/Cyclic/DoubleCyclic/DoubleSqrt.v index 4c93d758..d468318d 100644 --- a/theories/Numbers/Cyclic/DoubleCyclic/DoubleSqrt.v +++ b/theories/Numbers/Cyclic/DoubleCyclic/DoubleSqrt.v @@ -8,7 +8,7 @@ (* Benjamin Gregoire, Laurent Thery, INRIA, 2007 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: DoubleSqrt.v 13323 2010-07-24 15:57:30Z herbelin $ i*) Set Implicit Arguments. diff --git a/theories/Numbers/Cyclic/DoubleCyclic/DoubleSub.v b/theories/Numbers/Cyclic/DoubleCyclic/DoubleSub.v index 7ecec835..7cb97f28 100644 --- a/theories/Numbers/Cyclic/DoubleCyclic/DoubleSub.v +++ b/theories/Numbers/Cyclic/DoubleCyclic/DoubleSub.v @@ -8,7 +8,7 @@ (* Benjamin Gregoire, Laurent Thery, INRIA, 2007 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: DoubleSub.v 13323 2010-07-24 15:57:30Z herbelin $ i*) Set Implicit Arguments. diff --git a/theories/Numbers/Cyclic/DoubleCyclic/DoubleType.v b/theories/Numbers/Cyclic/DoubleCyclic/DoubleType.v index dde0c142..e9955c6d 100644 --- a/theories/Numbers/Cyclic/DoubleCyclic/DoubleType.v +++ b/theories/Numbers/Cyclic/DoubleCyclic/DoubleType.v @@ -8,7 +8,7 @@ (* Benjamin Gregoire, Laurent Thery, INRIA, 2007 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: DoubleType.v 13323 2010-07-24 15:57:30Z herbelin $ i*) Set Implicit Arguments. diff --git a/theories/Numbers/Cyclic/Int31/Cyclic31.v b/theories/Numbers/Cyclic/Int31/Cyclic31.v index f581657e..8ec359a0 100644 --- a/theories/Numbers/Cyclic/Int31/Cyclic31.v +++ b/theories/Numbers/Cyclic/Int31/Cyclic31.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: Cyclic31.v 13323 2010-07-24 15:57:30Z herbelin $ i*) (** * Int31 numbers defines indeed a cyclic structure : Z/(2^31)Z *) diff --git a/theories/Numbers/Cyclic/Int31/Int31.v b/theories/Numbers/Cyclic/Int31/Int31.v index 3c72b785..2485c353 100644 --- a/theories/Numbers/Cyclic/Int31/Int31.v +++ b/theories/Numbers/Cyclic/Int31/Int31.v @@ -8,7 +8,7 @@ (* Benjamin Gregoire, Laurent Thery, INRIA, 2007 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: Int31.v 13323 2010-07-24 15:57:30Z herbelin $ i*) Require Import NaryFunctions. Require Import Wf_nat. diff --git a/theories/Numbers/Cyclic/Int31/Ring31.v b/theories/Numbers/Cyclic/Int31/Ring31.v index ff55bc51..2864c81f 100644 --- a/theories/Numbers/Cyclic/Int31/Ring31.v +++ b/theories/Numbers/Cyclic/Int31/Ring31.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: Ring31.v 13323 2010-07-24 15:57:30Z herbelin $ i*) (** * Int31 numbers defines Z/(2^31)Z, and can hence be equipped with a ring structure and a ring tactic *) diff --git a/theories/Numbers/Cyclic/ZModulo/ZModulo.v b/theories/Numbers/Cyclic/ZModulo/ZModulo.v index ced812e2..bebc67a0 100644 --- a/theories/Numbers/Cyclic/ZModulo/ZModulo.v +++ b/theories/Numbers/Cyclic/ZModulo/ZModulo.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) +(* $Id: ZModulo.v 13323 2010-07-24 15:57:30Z herbelin $ *) (** * Type [Z] viewed modulo a particular constant corresponds to [Z/nZ] as defined abstractly in CyclicAxioms. *) diff --git a/theories/Numbers/Integer/Abstract/ZAdd.v b/theories/Numbers/Integer/Abstract/ZAdd.v index 71ca5e11..f120f881 100644 --- a/theories/Numbers/Integer/Abstract/ZAdd.v +++ b/theories/Numbers/Integer/Abstract/ZAdd.v @@ -8,7 +8,7 @@ (* Evgeny Makarov, INRIA, 2007 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: ZAdd.v 13323 2010-07-24 15:57:30Z herbelin $ i*) Require Export ZBase. diff --git a/theories/Numbers/Integer/Abstract/ZAddOrder.v b/theories/Numbers/Integer/Abstract/ZAddOrder.v index 96213eab..2d607010 100644 --- a/theories/Numbers/Integer/Abstract/ZAddOrder.v +++ b/theories/Numbers/Integer/Abstract/ZAddOrder.v @@ -8,7 +8,7 @@ (* Evgeny Makarov, INRIA, 2007 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: ZAddOrder.v 13323 2010-07-24 15:57:30Z herbelin $ i*) Require Export ZLt. diff --git a/theories/Numbers/Integer/Abstract/ZAxioms.v b/theories/Numbers/Integer/Abstract/ZAxioms.v index 13d32304..c52fe299 100644 --- a/theories/Numbers/Integer/Abstract/ZAxioms.v +++ b/theories/Numbers/Integer/Abstract/ZAxioms.v @@ -8,7 +8,7 @@ (* Evgeny Makarov, INRIA, 2007 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: ZAxioms.v 13323 2010-07-24 15:57:30Z herbelin $ i*) Require Export NZAxioms. diff --git a/theories/Numbers/Integer/Abstract/ZBase.v b/theories/Numbers/Integer/Abstract/ZBase.v index 244eb92c..a42e8230 100644 --- a/theories/Numbers/Integer/Abstract/ZBase.v +++ b/theories/Numbers/Integer/Abstract/ZBase.v @@ -8,7 +8,7 @@ (* Evgeny Makarov, INRIA, 2007 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: ZBase.v 13323 2010-07-24 15:57:30Z herbelin $ i*) Require Export Decidable. Require Export ZAxioms. diff --git a/theories/Numbers/Integer/Abstract/ZLt.v b/theories/Numbers/Integer/Abstract/ZLt.v index 14f2ef62..2e019a57 100644 --- a/theories/Numbers/Integer/Abstract/ZLt.v +++ b/theories/Numbers/Integer/Abstract/ZLt.v @@ -8,7 +8,7 @@ (* Evgeny Makarov, INRIA, 2007 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: ZLt.v 13323 2010-07-24 15:57:30Z herbelin $ i*) Require Export ZMul. diff --git a/theories/Numbers/Integer/Abstract/ZMul.v b/theories/Numbers/Integer/Abstract/ZMul.v index 5856c6d9..5be20268 100644 --- a/theories/Numbers/Integer/Abstract/ZMul.v +++ b/theories/Numbers/Integer/Abstract/ZMul.v @@ -8,7 +8,7 @@ (* Evgeny Makarov, INRIA, 2007 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: ZMul.v 13323 2010-07-24 15:57:30Z herbelin $ i*) Require Export ZAdd. diff --git a/theories/Numbers/Integer/Abstract/ZMulOrder.v b/theories/Numbers/Integer/Abstract/ZMulOrder.v index 69b9c986..d5ec8005 100644 --- a/theories/Numbers/Integer/Abstract/ZMulOrder.v +++ b/theories/Numbers/Integer/Abstract/ZMulOrder.v @@ -8,7 +8,7 @@ (* Evgeny Makarov, INRIA, 2007 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: ZMulOrder.v 13323 2010-07-24 15:57:30Z herbelin $ i*) Require Export ZAddOrder. diff --git a/theories/Numbers/Integer/Abstract/ZProperties.v b/theories/Numbers/Integer/Abstract/ZProperties.v index 7cc064d9..09ece42a 100644 --- a/theories/Numbers/Integer/Abstract/ZProperties.v +++ b/theories/Numbers/Integer/Abstract/ZProperties.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: ZProperties.v 13323 2010-07-24 15:57:30Z herbelin $ i*) Require Export ZAxioms ZMulOrder ZSgnAbs. diff --git a/theories/Numbers/Integer/BigZ/BigZ.v b/theories/Numbers/Integer/BigZ/BigZ.v index 180081d9..7f9e2d91 100644 --- a/theories/Numbers/Integer/BigZ/BigZ.v +++ b/theories/Numbers/Integer/BigZ/BigZ.v @@ -8,7 +8,7 @@ (* Benjamin Gregoire, Laurent Thery, INRIA, 2007 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: BigZ.v 13323 2010-07-24 15:57:30Z herbelin $ i*) Require Export BigN. Require Import ZProperties ZDivFloor ZSig ZSigZAxioms ZMake. diff --git a/theories/Numbers/Integer/BigZ/ZMake.v b/theories/Numbers/Integer/BigZ/ZMake.v index 70fe97d9..c61e198d 100644 --- a/theories/Numbers/Integer/BigZ/ZMake.v +++ b/theories/Numbers/Integer/BigZ/ZMake.v @@ -8,7 +8,7 @@ (* Benjamin Gregoire, Laurent Thery, INRIA, 2007 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: ZMake.v 13323 2010-07-24 15:57:30Z herbelin $ i*) Require Import ZArith. Require Import BigNumPrelude. diff --git a/theories/Numbers/Integer/Binary/ZBinary.v b/theories/Numbers/Integer/Binary/ZBinary.v index a904cdba..9c8f80c9 100644 --- a/theories/Numbers/Integer/Binary/ZBinary.v +++ b/theories/Numbers/Integer/Binary/ZBinary.v @@ -8,7 +8,7 @@ (* Evgeny Makarov, INRIA, 2007 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: ZBinary.v 13323 2010-07-24 15:57:30Z herbelin $ i*) Require Import ZAxioms ZProperties. diff --git a/theories/Numbers/Integer/NatPairs/ZNatPairs.v b/theories/Numbers/Integer/NatPairs/ZNatPairs.v index 45c5db77..830e1ad7 100644 --- a/theories/Numbers/Integer/NatPairs/ZNatPairs.v +++ b/theories/Numbers/Integer/NatPairs/ZNatPairs.v @@ -8,7 +8,7 @@ (* Evgeny Makarov, INRIA, 2007 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: ZNatPairs.v 13323 2010-07-24 15:57:30Z herbelin $ i*) Require Import NProperties. (* The most complete file for N *) Require Export ZProperties. (* The most complete file for Z *) diff --git a/theories/Numbers/Integer/SpecViaZ/ZSig.v b/theories/Numbers/Integer/SpecViaZ/ZSig.v index b2c23685..957e1c70 100644 --- a/theories/Numbers/Integer/SpecViaZ/ZSig.v +++ b/theories/Numbers/Integer/SpecViaZ/ZSig.v @@ -8,7 +8,7 @@ (* Benjamin Gregoire, Laurent Thery, INRIA, 2007 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: ZSig.v 13323 2010-07-24 15:57:30Z herbelin $ i*) Require Import ZArith Znumtheory. diff --git a/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v b/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v index bb8d543e..142e613b 100644 --- a/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v +++ b/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: ZSigZAxioms.v 13323 2010-07-24 15:57:30Z herbelin $ i*) Require Import ZArith ZAxioms ZDivFloor ZSig. diff --git a/theories/Numbers/NaryFunctions.v b/theories/Numbers/NaryFunctions.v index 83487d22..b0aad5b5 100644 --- a/theories/Numbers/NaryFunctions.v +++ b/theories/Numbers/NaryFunctions.v @@ -8,7 +8,7 @@ (* Pierre Letouzey, Jerome Vouillon, PPS, Paris 7, 2008 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: NaryFunctions.v 13323 2010-07-24 15:57:30Z herbelin $ i*) Local Open Scope type_scope. diff --git a/theories/Numbers/NatInt/NZAdd.v b/theories/Numbers/NatInt/NZAdd.v index ee73a22a..6f1b879c 100644 --- a/theories/Numbers/NatInt/NZAdd.v +++ b/theories/Numbers/NatInt/NZAdd.v @@ -8,7 +8,7 @@ (* Evgeny Makarov, INRIA, 2007 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: NZAdd.v 13323 2010-07-24 15:57:30Z herbelin $ i*) Require Import NZAxioms NZBase. diff --git a/theories/Numbers/NatInt/NZAddOrder.v b/theories/Numbers/NatInt/NZAddOrder.v index ca359346..7c06226f 100644 --- a/theories/Numbers/NatInt/NZAddOrder.v +++ b/theories/Numbers/NatInt/NZAddOrder.v @@ -8,7 +8,7 @@ (* Evgeny Makarov, INRIA, 2007 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: NZAddOrder.v 13323 2010-07-24 15:57:30Z herbelin $ i*) Require Import NZAxioms NZBase NZMul NZOrder. diff --git a/theories/Numbers/NatInt/NZAxioms.v b/theories/Numbers/NatInt/NZAxioms.v index bb13d051..389f4eb2 100644 --- a/theories/Numbers/NatInt/NZAxioms.v +++ b/theories/Numbers/NatInt/NZAxioms.v @@ -8,7 +8,7 @@ (** Initial Author : Evgeny Makarov, INRIA, 2007 *) -(*i $Id$ i*) +(*i $Id: NZAxioms.v 13323 2010-07-24 15:57:30Z herbelin $ i*) Require Export Equalities Orders NumPrelude GenericMinMax. diff --git a/theories/Numbers/NatInt/NZBase.v b/theories/Numbers/NatInt/NZBase.v index f83af8f0..b5df1669 100644 --- a/theories/Numbers/NatInt/NZBase.v +++ b/theories/Numbers/NatInt/NZBase.v @@ -8,7 +8,7 @@ (* Evgeny Makarov, INRIA, 2007 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: NZBase.v 13323 2010-07-24 15:57:30Z herbelin $ i*) Require Import NZAxioms. diff --git a/theories/Numbers/NatInt/NZDomain.v b/theories/Numbers/NatInt/NZDomain.v index d8e45ff5..af3e4861 100644 --- a/theories/Numbers/NatInt/NZDomain.v +++ b/theories/Numbers/NatInt/NZDomain.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: NZDomain.v 13323 2010-07-24 15:57:30Z herbelin $ i*) Require Export NumPrelude NZAxioms. Require Import NZBase NZOrder NZAddOrder Plus Minus. diff --git a/theories/Numbers/NatInt/NZMul.v b/theories/Numbers/NatInt/NZMul.v index 14981a22..b55f58cb 100644 --- a/theories/Numbers/NatInt/NZMul.v +++ b/theories/Numbers/NatInt/NZMul.v @@ -8,7 +8,7 @@ (* Evgeny Makarov, INRIA, 2007 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: NZMul.v 13323 2010-07-24 15:57:30Z herbelin $ i*) Require Import NZAxioms NZBase NZAdd. diff --git a/theories/Numbers/NatInt/NZMulOrder.v b/theories/Numbers/NatInt/NZMulOrder.v index 35922519..dee1a803 100644 --- a/theories/Numbers/NatInt/NZMulOrder.v +++ b/theories/Numbers/NatInt/NZMulOrder.v @@ -8,7 +8,7 @@ (* Evgeny Makarov, INRIA, 2007 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: NZMulOrder.v 13323 2010-07-24 15:57:30Z herbelin $ i*) Require Import NZAxioms. Require Import NZAddOrder. diff --git a/theories/Numbers/NatInt/NZOrder.v b/theories/Numbers/NatInt/NZOrder.v index 3f00cd20..5d7bb701 100644 --- a/theories/Numbers/NatInt/NZOrder.v +++ b/theories/Numbers/NatInt/NZOrder.v @@ -8,7 +8,7 @@ (* Evgeny Makarov, INRIA, 2007 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: NZOrder.v 13323 2010-07-24 15:57:30Z herbelin $ i*) Require Import NZAxioms NZBase Decidable OrdersTac. diff --git a/theories/Numbers/NatInt/NZProperties.v b/theories/Numbers/NatInt/NZProperties.v index 7a7601bd..92dffed3 100644 --- a/theories/Numbers/NatInt/NZProperties.v +++ b/theories/Numbers/NatInt/NZProperties.v @@ -8,7 +8,7 @@ (* Evgeny Makarov, INRIA, 2007 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: NZProperties.v 13323 2010-07-24 15:57:30Z herbelin $ i*) Require Export NZAxioms NZMulOrder. diff --git a/theories/Numbers/Natural/Abstract/NAdd.v b/theories/Numbers/Natural/Abstract/NAdd.v index 4ae8b393..305ccfd0 100644 --- a/theories/Numbers/Natural/Abstract/NAdd.v +++ b/theories/Numbers/Natural/Abstract/NAdd.v @@ -8,7 +8,7 @@ (* Evgeny Makarov, INRIA, 2007 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: NAdd.v 13323 2010-07-24 15:57:30Z herbelin $ i*) Require Export NBase. diff --git a/theories/Numbers/Natural/Abstract/NAddOrder.v b/theories/Numbers/Natural/Abstract/NAddOrder.v index 729618ef..a4b8c759 100644 --- a/theories/Numbers/Natural/Abstract/NAddOrder.v +++ b/theories/Numbers/Natural/Abstract/NAddOrder.v @@ -8,7 +8,7 @@ (* Evgeny Makarov, INRIA, 2007 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: NAddOrder.v 13323 2010-07-24 15:57:30Z herbelin $ i*) Require Export NOrder. diff --git a/theories/Numbers/Natural/Abstract/NAxioms.v b/theories/Numbers/Natural/Abstract/NAxioms.v index 309dff8f..1a7c436b 100644 --- a/theories/Numbers/Natural/Abstract/NAxioms.v +++ b/theories/Numbers/Natural/Abstract/NAxioms.v @@ -8,7 +8,7 @@ (* Evgeny Makarov, INRIA, 2007 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: NAxioms.v 13323 2010-07-24 15:57:30Z herbelin $ i*) Require Export NZAxioms. diff --git a/theories/Numbers/Natural/Abstract/NBase.v b/theories/Numbers/Natural/Abstract/NBase.v index 48bdfabf..5f262a82 100644 --- a/theories/Numbers/Natural/Abstract/NBase.v +++ b/theories/Numbers/Natural/Abstract/NBase.v @@ -8,7 +8,7 @@ (* Evgeny Makarov, INRIA, 2007 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: NBase.v 13323 2010-07-24 15:57:30Z herbelin $ i*) Require Export Decidable. Require Export NAxioms. diff --git a/theories/Numbers/Natural/Abstract/NDefOps.v b/theories/Numbers/Natural/Abstract/NDefOps.v index ca2b1b7e..238518ba 100644 --- a/theories/Numbers/Natural/Abstract/NDefOps.v +++ b/theories/Numbers/Natural/Abstract/NDefOps.v @@ -8,7 +8,7 @@ (* Evgeny Makarov, INRIA, 2007 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: NDefOps.v 13323 2010-07-24 15:57:30Z herbelin $ i*) Require Import Bool. (* To get the orb and negb function *) Require Import RelationPairs. diff --git a/theories/Numbers/Natural/Abstract/NIso.v b/theories/Numbers/Natural/Abstract/NIso.v index c3e5e27c..79516623 100644 --- a/theories/Numbers/Natural/Abstract/NIso.v +++ b/theories/Numbers/Natural/Abstract/NIso.v @@ -8,7 +8,7 @@ (* Evgeny Makarov, INRIA, 2007 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: NIso.v 13323 2010-07-24 15:57:30Z herbelin $ i*) Require Import NBase. diff --git a/theories/Numbers/Natural/Abstract/NMulOrder.v b/theories/Numbers/Natural/Abstract/NMulOrder.v index 9471ac6c..2b00e893 100644 --- a/theories/Numbers/Natural/Abstract/NMulOrder.v +++ b/theories/Numbers/Natural/Abstract/NMulOrder.v @@ -8,7 +8,7 @@ (* Evgeny Makarov, INRIA, 2007 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: NMulOrder.v 13323 2010-07-24 15:57:30Z herbelin $ i*) Require Export NAddOrder. diff --git a/theories/Numbers/Natural/Abstract/NOrder.v b/theories/Numbers/Natural/Abstract/NOrder.v index 766facd5..cebf35a7 100644 --- a/theories/Numbers/Natural/Abstract/NOrder.v +++ b/theories/Numbers/Natural/Abstract/NOrder.v @@ -8,7 +8,7 @@ (* Evgeny Makarov, INRIA, 2007 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: NOrder.v 13323 2010-07-24 15:57:30Z herbelin $ i*) Require Export NAdd. diff --git a/theories/Numbers/Natural/Abstract/NProperties.v b/theories/Numbers/Natural/Abstract/NProperties.v index f20c352e..3269972d 100644 --- a/theories/Numbers/Natural/Abstract/NProperties.v +++ b/theories/Numbers/Natural/Abstract/NProperties.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: NProperties.v 13323 2010-07-24 15:57:30Z herbelin $ i*) Require Export NAxioms NSub. diff --git a/theories/Numbers/Natural/Abstract/NStrongRec.v b/theories/Numbers/Natural/Abstract/NStrongRec.v index 86e1d93a..f5f47128 100644 --- a/theories/Numbers/Natural/Abstract/NStrongRec.v +++ b/theories/Numbers/Natural/Abstract/NStrongRec.v @@ -8,7 +8,7 @@ (* Evgeny Makarov, INRIA, 2007 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: NStrongRec.v 13323 2010-07-24 15:57:30Z herbelin $ i*) (** This file defined the strong (course-of-value, well-founded) recursion and proves its properties *) diff --git a/theories/Numbers/Natural/Abstract/NSub.v b/theories/Numbers/Natural/Abstract/NSub.v index 8df327d6..8d16c516 100644 --- a/theories/Numbers/Natural/Abstract/NSub.v +++ b/theories/Numbers/Natural/Abstract/NSub.v @@ -8,7 +8,7 @@ (* Evgeny Makarov, INRIA, 2007 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: NSub.v 13323 2010-07-24 15:57:30Z herbelin $ i*) Require Export NMulOrder. diff --git a/theories/Numbers/Natural/BigN/NMake_gen.ml b/theories/Numbers/Natural/BigN/NMake_gen.ml index 5bcf5e9a..8f6c59fd 100644 --- a/theories/Numbers/Natural/BigN/NMake_gen.ml +++ b/theories/Numbers/Natural/BigN/NMake_gen.ml @@ -8,7 +8,7 @@ (* Benjamin Gregoire, Laurent Thery, INRIA, 2007 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: NMake_gen.ml 13323 2010-07-24 15:57:30Z herbelin $ i*) (*S NMake_gen.ml : this file generates NMake.v *) diff --git a/theories/Numbers/Natural/BigN/Nbasic.v b/theories/Numbers/Natural/BigN/Nbasic.v index 163712b6..a531b92e 100644 --- a/theories/Numbers/Natural/BigN/Nbasic.v +++ b/theories/Numbers/Natural/BigN/Nbasic.v @@ -8,7 +8,7 @@ (* Benjamin Gregoire, Laurent Thery, INRIA, 2007 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: Nbasic.v 13323 2010-07-24 15:57:30Z herbelin $ i*) Require Import ZArith. Require Import BigNumPrelude. diff --git a/theories/Numbers/Natural/Binary/NBinary.v b/theories/Numbers/Natural/Binary/NBinary.v index 1fae59eb..b83e5477 100644 --- a/theories/Numbers/Natural/Binary/NBinary.v +++ b/theories/Numbers/Natural/Binary/NBinary.v @@ -8,7 +8,7 @@ (* Evgeny Makarov, INRIA, 2007 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: NBinary.v 13323 2010-07-24 15:57:30Z herbelin $ i*) Require Import BinPos. Require Export BinNat. diff --git a/theories/Numbers/Natural/Peano/NPeano.v b/theories/Numbers/Natural/Peano/NPeano.v index 5b468a90..4a5364fd 100644 --- a/theories/Numbers/Natural/Peano/NPeano.v +++ b/theories/Numbers/Natural/Peano/NPeano.v @@ -8,7 +8,7 @@ (* Evgeny Makarov, INRIA, 2007 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: NPeano.v 13323 2010-07-24 15:57:30Z herbelin $ i*) Require Import Arith MinMax NAxioms NProperties. diff --git a/theories/Numbers/Natural/SpecViaZ/NSig.v b/theories/Numbers/Natural/SpecViaZ/NSig.v index 6ccbd2f0..89111937 100644 --- a/theories/Numbers/Natural/SpecViaZ/NSig.v +++ b/theories/Numbers/Natural/SpecViaZ/NSig.v @@ -8,7 +8,7 @@ (* Benjamin Gregoire, Laurent Thery, INRIA, 2007 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: NSig.v 13323 2010-07-24 15:57:30Z herbelin $ i*) Require Import ZArith Znumtheory. diff --git a/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v b/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v index 73e7953f..2c35242a 100644 --- a/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v +++ b/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: NSigNAxioms.v 13323 2010-07-24 15:57:30Z herbelin $ i*) Require Import ZArith Nnat NAxioms NDiv NSig. diff --git a/theories/Numbers/NumPrelude.v b/theories/Numbers/NumPrelude.v index 69f6e24b..f923a53b 100644 --- a/theories/Numbers/NumPrelude.v +++ b/theories/Numbers/NumPrelude.v @@ -8,7 +8,7 @@ (* Evgeny Makarov, INRIA, 2007 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: NumPrelude.v 13323 2010-07-24 15:57:30Z herbelin $ i*) Require Export Setoid Morphisms. diff --git a/theories/Numbers/Rational/SpecViaQ/QSig.v b/theories/Numbers/Rational/SpecViaQ/QSig.v index 0982226c..10d0c5f7 100644 --- a/theories/Numbers/Rational/SpecViaQ/QSig.v +++ b/theories/Numbers/Rational/SpecViaQ/QSig.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: QSig.v 13323 2010-07-24 15:57:30Z herbelin $ i*) Require Import QArith Qpower Qminmax Orders RelationPairs GenericMinMax. diff --git a/theories/Program/Basics.v b/theories/Program/Basics.v index f4017024..a298032f 100644 --- a/theories/Program/Basics.v +++ b/theories/Program/Basics.v @@ -6,7 +6,7 @@ (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) +(* $Id: Basics.v 13323 2010-07-24 15:57:30Z herbelin $ *) (** Standard functions and combinators. diff --git a/theories/Program/Combinators.v b/theories/Program/Combinators.v index 39fb4093..e61c7027 100644 --- a/theories/Program/Combinators.v +++ b/theories/Program/Combinators.v @@ -6,7 +6,7 @@ (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) +(* $Id: Combinators.v 13323 2010-07-24 15:57:30Z herbelin $ *) (** * Proofs about standard combinators, exports functional extensionality. diff --git a/theories/Program/Equality.v b/theories/Program/Equality.v index 1e139497..2764d1b4 100644 --- a/theories/Program/Equality.v +++ b/theories/Program/Equality.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: Equality.v 13359 2010-07-30 08:46:55Z herbelin $ i*) (** Tactics related to (dependent) equality and proof irrelevance. *) @@ -15,6 +15,9 @@ Require Export JMeq. Require Import Coq.Program.Tactics. +Local Notation "'Π' x .. y , P" := (forall x, .. (forall y, P) ..) + (at level 200, x binder, y binder, right associativity) : type_scope. + Ltac is_ground_goal := match goal with |- ?T => is_ground T diff --git a/theories/Program/Program.v b/theories/Program/Program.v index 71be3478..929fc47c 100644 --- a/theories/Program/Program.v +++ b/theories/Program/Program.v @@ -5,7 +5,7 @@ (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) +(* $Id: Program.v 13323 2010-07-24 15:57:30Z herbelin $ *) Require Export Coq.Program.Utils. Require Export Coq.Program.Wf. diff --git a/theories/Program/Subset.v b/theories/Program/Subset.v index ce5f1068..9d82fde8 100644 --- a/theories/Program/Subset.v +++ b/theories/Program/Subset.v @@ -5,7 +5,7 @@ (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) +(* $Id: Subset.v 13323 2010-07-24 15:57:30Z herbelin $ *) (** Tactics related to subsets and proof irrelevance. *) diff --git a/theories/Program/Syntax.v b/theories/Program/Syntax.v index 05bf2ea6..0e6b2909 100644 --- a/theories/Program/Syntax.v +++ b/theories/Program/Syntax.v @@ -5,7 +5,7 @@ (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) +(* $Id: Syntax.v 13323 2010-07-24 15:57:30Z herbelin $ *) (** Custom notations and implicits for Coq prelude definitions. diff --git a/theories/Program/Tactics.v b/theories/Program/Tactics.v index 91a8edff..333dd7a6 100644 --- a/theories/Program/Tactics.v +++ b/theories/Program/Tactics.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: Tactics.v 13332 2010-07-26 22:12:43Z msozeau $ i*) (** This module implements various tactics used to simplify the goals produced by Program, which are also generally useful. *) @@ -101,7 +101,7 @@ Ltac revert_last := [ H : _ |- _ ] => revert H end. -(** Reapeateadly reverse the last hypothesis, putting everything in the goal. *) +(** Repeatedly reverse the last hypothesis, putting everything in the goal. *) Ltac reverse := repeat revert_last. diff --git a/theories/Program/Utils.v b/theories/Program/Utils.v index f2aad800..b2b5d4be 100644 --- a/theories/Program/Utils.v +++ b/theories/Program/Utils.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: Utils.v 13323 2010-07-24 15:57:30Z herbelin $ i*) (** Various syntaxic shortands that are useful with [Program]. *) diff --git a/theories/Program/Wf.v b/theories/Program/Wf.v index d16e900f..4159f436 100644 --- a/theories/Program/Wf.v +++ b/theories/Program/Wf.v @@ -5,7 +5,7 @@ (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) +(* $Id: Wf.v 13332 2010-07-26 22:12:43Z msozeau $ *) (** Reformulation of the Wf module using subsets where possible, providing the support for [Program]'s treatment of well-founded definitions. *) @@ -214,7 +214,7 @@ Ltac fold_sub f := match goal with | [ |- ?T ] => match T with - appcontext C [ @Fix_sub _ _ _ _ ?arg ] => + appcontext C [ @Fix_sub _ _ _ _ _ ?arg ] => let app := context C [ f arg ] in change app end @@ -251,6 +251,6 @@ Module WfExtensionality. Ltac unfold_sub f fargs := set (call:=fargs) ; unfold f in call ; unfold call ; clear call ; - rewrite fix_sub_eq_ext ; repeat fold_sub fargs ; simpl proj1_sig. + rewrite fix_sub_eq_ext ; repeat fold_sub f ; simpl proj1_sig. End WfExtensionality. diff --git a/theories/QArith/QArith.v b/theories/QArith/QArith.v index 1b3ca6d6..c7f41de4 100644 --- a/theories/QArith/QArith.v +++ b/theories/QArith/QArith.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: QArith.v 13323 2010-07-24 15:57:30Z herbelin $ i*) Require Export QArith_base. Require Export Qring. diff --git a/theories/QArith/QArith_base.v b/theories/QArith/QArith_base.v index 9540968d..6b33c254 100644 --- a/theories/QArith/QArith_base.v +++ b/theories/QArith/QArith_base.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: QArith_base.v 13323 2010-07-24 15:57:30Z herbelin $ i*) Require Export ZArith. Require Export ZArithRing. diff --git a/theories/QArith/Qcanon.v b/theories/QArith/Qcanon.v index eb1508b3..4a2347d7 100644 --- a/theories/QArith/Qcanon.v +++ b/theories/QArith/Qcanon.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: Qcanon.v 13323 2010-07-24 15:57:30Z herbelin $ i*) Require Import Field. Require Import QArith. diff --git a/theories/QArith/Qfield.v b/theories/QArith/Qfield.v index 00500e31..0cf5413e 100644 --- a/theories/QArith/Qfield.v +++ b/theories/QArith/Qfield.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: Qfield.v 13323 2010-07-24 15:57:30Z herbelin $ i*) Require Export Field. Require Export QArith_base. diff --git a/theories/QArith/Qreals.v b/theories/QArith/Qreals.v index 54682197..67bb0ffa 100644 --- a/theories/QArith/Qreals.v +++ b/theories/QArith/Qreals.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: Qreals.v 13323 2010-07-24 15:57:30Z herbelin $ i*) Require Export Rbase. Require Export QArith_base. diff --git a/theories/QArith/Qreduction.v b/theories/QArith/Qreduction.v index 2fa2585d..456d305d 100644 --- a/theories/QArith/Qreduction.v +++ b/theories/QArith/Qreduction.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: Qreduction.v 13323 2010-07-24 15:57:30Z herbelin $ i*) (** Normalisation functions for rational numbers. *) diff --git a/theories/QArith/Qring.v b/theories/QArith/Qring.v index 8943dc31..7f7a2d09 100644 --- a/theories/QArith/Qring.v +++ b/theories/QArith/Qring.v @@ -6,6 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: Qring.v 13323 2010-07-24 15:57:30Z herbelin $ i*) Require Export Qfield. diff --git a/theories/Reals/Alembert.v b/theories/Reals/Alembert.v index dbee0b67..212eea7a 100644 --- a/theories/Reals/Alembert.v +++ b/theories/Reals/Alembert.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: Alembert.v 13323 2010-07-24 15:57:30Z herbelin $ i*) Require Import Rbase. Require Import Rfunctions. diff --git a/theories/Reals/AltSeries.v b/theories/Reals/AltSeries.v index e17bf53d..de9f8827 100644 --- a/theories/Reals/AltSeries.v +++ b/theories/Reals/AltSeries.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) - (*i $Id$ i*) + (*i $Id: AltSeries.v 13323 2010-07-24 15:57:30Z herbelin $ i*) Require Import Rbase. Require Import Rfunctions. diff --git a/theories/Reals/ArithProp.v b/theories/Reals/ArithProp.v index c0f7e830..84fa8fe1 100644 --- a/theories/Reals/ArithProp.v +++ b/theories/Reals/ArithProp.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) - (*i $Id$ i*) + (*i $Id: ArithProp.v 13323 2010-07-24 15:57:30Z herbelin $ i*) Require Import Rbase. Require Import Rbasic_fun. diff --git a/theories/Reals/Binomial.v b/theories/Reals/Binomial.v index 9e3ffa6d..ab352910 100644 --- a/theories/Reals/Binomial.v +++ b/theories/Reals/Binomial.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) - (*i $Id$ i*) + (*i $Id: Binomial.v 13323 2010-07-24 15:57:30Z herbelin $ i*) Require Import Rbase. Require Import Rfunctions. diff --git a/theories/Reals/Cauchy_prod.v b/theories/Reals/Cauchy_prod.v index 713e2c04..279fd3d1 100644 --- a/theories/Reals/Cauchy_prod.v +++ b/theories/Reals/Cauchy_prod.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) - (*i $Id$ i*) + (*i $Id: Cauchy_prod.v 13323 2010-07-24 15:57:30Z herbelin $ i*) Require Import Rbase. Require Import Rfunctions. diff --git a/theories/Reals/Cos_plus.v b/theories/Reals/Cos_plus.v index 4e4c2b60..e3854afb 100644 --- a/theories/Reals/Cos_plus.v +++ b/theories/Reals/Cos_plus.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) - (*i $Id$ i*) + (*i $Id: Cos_plus.v 13323 2010-07-24 15:57:30Z herbelin $ i*) Require Import Rbase. Require Import Rfunctions. diff --git a/theories/Reals/Cos_rel.v b/theories/Reals/Cos_rel.v index 54332d83..99e39169 100644 --- a/theories/Reals/Cos_rel.v +++ b/theories/Reals/Cos_rel.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: Cos_rel.v 13323 2010-07-24 15:57:30Z herbelin $ i*) Require Import Rbase. Require Import Rfunctions. diff --git a/theories/Reals/DiscrR.v b/theories/Reals/DiscrR.v index 08b48898..66ee4eb0 100644 --- a/theories/Reals/DiscrR.v +++ b/theories/Reals/DiscrR.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: DiscrR.v 13323 2010-07-24 15:57:30Z herbelin $ i*) Require Import RIneq. Require Import Omega. diff --git a/theories/Reals/Exp_prop.v b/theories/Reals/Exp_prop.v index 5d46ceae..57198a5e 100644 --- a/theories/Reals/Exp_prop.v +++ b/theories/Reals/Exp_prop.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: Exp_prop.v 13323 2010-07-24 15:57:30Z herbelin $ i*) Require Import Rbase. Require Import Rfunctions. diff --git a/theories/Reals/Integration.v b/theories/Reals/Integration.v index 2062db7d..569e122a 100644 --- a/theories/Reals/Integration.v +++ b/theories/Reals/Integration.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: Integration.v 13323 2010-07-24 15:57:30Z herbelin $ i*) Require Export NewtonInt. Require Export RiemannInt_SF. diff --git a/theories/Reals/LegacyRfield.v b/theories/Reals/LegacyRfield.v index a4bb5f72..1528ed64 100644 --- a/theories/Reals/LegacyRfield.v +++ b/theories/Reals/LegacyRfield.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: LegacyRfield.v 13323 2010-07-24 15:57:30Z herbelin $ i*) Require Export Raxioms. Require Export LegacyField. diff --git a/theories/Reals/MVT.v b/theories/Reals/MVT.v index d69e7ed5..87275e7f 100644 --- a/theories/Reals/MVT.v +++ b/theories/Reals/MVT.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: MVT.v 13323 2010-07-24 15:57:30Z herbelin $ i*) Require Import Rbase. Require Import Rfunctions. diff --git a/theories/Reals/NewtonInt.v b/theories/Reals/NewtonInt.v index 8828c7eb..cfd5d561 100644 --- a/theories/Reals/NewtonInt.v +++ b/theories/Reals/NewtonInt.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: NewtonInt.v 13323 2010-07-24 15:57:30Z herbelin $ i*) Require Import Rbase. Require Import Rfunctions. diff --git a/theories/Reals/PSeries_reg.v b/theories/Reals/PSeries_reg.v index a459fe19..1e882b7a 100644 --- a/theories/Reals/PSeries_reg.v +++ b/theories/Reals/PSeries_reg.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: PSeries_reg.v 13323 2010-07-24 15:57:30Z herbelin $ i*) Require Import Rbase. Require Import Rfunctions. diff --git a/theories/Reals/PartSum.v b/theories/Reals/PartSum.v index e658b900..b1c0c4f9 100644 --- a/theories/Reals/PartSum.v +++ b/theories/Reals/PartSum.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: PartSum.v 13323 2010-07-24 15:57:30Z herbelin $ i*) Require Import Rbase. Require Import Rfunctions. diff --git a/theories/Reals/RIneq.v b/theories/Reals/RIneq.v index 55e14289..5c0cf3e7 100644 --- a/theories/Reals/RIneq.v +++ b/theories/Reals/RIneq.v @@ -7,7 +7,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: RIneq.v 13323 2010-07-24 15:57:30Z herbelin $ i*) (*********************************************************) (** * Basic lemmas for the classical real numbers *) diff --git a/theories/Reals/RList.v b/theories/Reals/RList.v index 36d04297..85ad4378 100644 --- a/theories/Reals/RList.v +++ b/theories/Reals/RList.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: RList.v 13323 2010-07-24 15:57:30Z herbelin $ i*) Require Import Rbase. Require Import Rfunctions. diff --git a/theories/Reals/R_Ifp.v b/theories/Reals/R_Ifp.v index cf7bdfef..946a8833 100644 --- a/theories/Reals/R_Ifp.v +++ b/theories/Reals/R_Ifp.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: R_Ifp.v 13323 2010-07-24 15:57:30Z herbelin $ i*) (**********************************************************) (** Complements for the reals.Integer and fractional part *) diff --git a/theories/Reals/R_sqr.v b/theories/Reals/R_sqr.v index fc8149fb..317f523b 100644 --- a/theories/Reals/R_sqr.v +++ b/theories/Reals/R_sqr.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: R_sqr.v 13323 2010-07-24 15:57:30Z herbelin $ i*) Require Import Rbase. Require Import Rbasic_fun. diff --git a/theories/Reals/R_sqrt.v b/theories/Reals/R_sqrt.v index ccecafc1..6eab48c0 100644 --- a/theories/Reals/R_sqrt.v +++ b/theories/Reals/R_sqrt.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: R_sqrt.v 13323 2010-07-24 15:57:30Z herbelin $ i*) Require Import Rbase. Require Import Rfunctions. diff --git a/theories/Reals/Ranalysis.v b/theories/Reals/Ranalysis.v index 17c6e90c..885d97ac 100644 --- a/theories/Reals/Ranalysis.v +++ b/theories/Reals/Ranalysis.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: Ranalysis.v 13323 2010-07-24 15:57:30Z herbelin $ i*) Require Import Rbase. Require Import Rfunctions. diff --git a/theories/Reals/Ranalysis1.v b/theories/Reals/Ranalysis1.v index 5d0a7f5a..def01d6f 100644 --- a/theories/Reals/Ranalysis1.v +++ b/theories/Reals/Ranalysis1.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: Ranalysis1.v 13323 2010-07-24 15:57:30Z herbelin $ i*) Require Import Rbase. Require Import Rfunctions. diff --git a/theories/Reals/Ranalysis2.v b/theories/Reals/Ranalysis2.v index 838fbaed..b8610d12 100644 --- a/theories/Reals/Ranalysis2.v +++ b/theories/Reals/Ranalysis2.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: Ranalysis2.v 13323 2010-07-24 15:57:30Z herbelin $ i*) Require Import Rbase. Require Import Rfunctions. diff --git a/theories/Reals/Ranalysis3.v b/theories/Reals/Ranalysis3.v index 3925b33c..1848ca52 100644 --- a/theories/Reals/Ranalysis3.v +++ b/theories/Reals/Ranalysis3.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: Ranalysis3.v 13323 2010-07-24 15:57:30Z herbelin $ i*) Require Import Rbase. Require Import Rfunctions. diff --git a/theories/Reals/Ranalysis4.v b/theories/Reals/Ranalysis4.v index 78d37a1f..97b6d52b 100644 --- a/theories/Reals/Ranalysis4.v +++ b/theories/Reals/Ranalysis4.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: Ranalysis4.v 13323 2010-07-24 15:57:30Z herbelin $ i*) Require Import Rbase. Require Import Rfunctions. diff --git a/theories/Reals/Raxioms.v b/theories/Reals/Raxioms.v index f7278562..dca2782c 100644 --- a/theories/Reals/Raxioms.v +++ b/theories/Reals/Raxioms.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: Raxioms.v 13323 2010-07-24 15:57:30Z herbelin $ i*) (*********************************************************) (** Axiomatisation of the classical reals *) diff --git a/theories/Reals/Rbase.v b/theories/Reals/Rbase.v index e3e36b11..ab005daf 100644 --- a/theories/Reals/Rbase.v +++ b/theories/Reals/Rbase.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: Rbase.v 13323 2010-07-24 15:57:30Z herbelin $ i*) Require Export Rdefinitions. Require Export Raxioms. diff --git a/theories/Reals/Rbasic_fun.v b/theories/Reals/Rbasic_fun.v index 241232e9..39f2bf6f 100644 --- a/theories/Reals/Rbasic_fun.v +++ b/theories/Reals/Rbasic_fun.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: Rbasic_fun.v 13323 2010-07-24 15:57:30Z herbelin $ i*) (*********************************************************) (** Complements for the real numbers *) diff --git a/theories/Reals/Rcomplete.v b/theories/Reals/Rcomplete.v index af91ae3d..6e66e904 100644 --- a/theories/Reals/Rcomplete.v +++ b/theories/Reals/Rcomplete.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: Rcomplete.v 13323 2010-07-24 15:57:30Z herbelin $ i*) Require Import Rbase. Require Import Rfunctions. diff --git a/theories/Reals/Rdefinitions.v b/theories/Reals/Rdefinitions.v index 311c7a26..301e0dcf 100644 --- a/theories/Reals/Rdefinitions.v +++ b/theories/Reals/Rdefinitions.v @@ -5,7 +5,7 @@ (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: Rdefinitions.v 13323 2010-07-24 15:57:30Z herbelin $ i*) (*********************************************************) diff --git a/theories/Reals/Rderiv.v b/theories/Reals/Rderiv.v index 7aa26fca..2b8c95f7 100644 --- a/theories/Reals/Rderiv.v +++ b/theories/Reals/Rderiv.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: Rderiv.v 13323 2010-07-24 15:57:30Z herbelin $ i*) (*********************************************************) (** Definition of the derivative,continuity *) diff --git a/theories/Reals/Reals.v b/theories/Reals/Reals.v index 3621a7da..f0ce1353 100644 --- a/theories/Reals/Reals.v +++ b/theories/Reals/Reals.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: Reals.v 13323 2010-07-24 15:57:30Z herbelin $ i*) (** The library REALS is divided in 6 parts : - Rbase: basic lemmas on R diff --git a/theories/Reals/Rfunctions.v b/theories/Reals/Rfunctions.v index 2e028411..f56b68c6 100644 --- a/theories/Reals/Rfunctions.v +++ b/theories/Reals/Rfunctions.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: Rfunctions.v 13323 2010-07-24 15:57:30Z herbelin $ i*) (*i Some properties about pow and sum have been made with John Harrison i*) (*i Some Lemmas (about pow and powerRZ) have been done by Laurent Thery i*) diff --git a/theories/Reals/Rgeom.v b/theories/Reals/Rgeom.v index 5f96d5e7..703ecfd4 100644 --- a/theories/Reals/Rgeom.v +++ b/theories/Reals/Rgeom.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: Rgeom.v 13323 2010-07-24 15:57:30Z herbelin $ i*) Require Import Rbase. Require Import Rfunctions. diff --git a/theories/Reals/RiemannInt.v b/theories/Reals/RiemannInt.v index 53a81ac2..4534a468 100644 --- a/theories/Reals/RiemannInt.v +++ b/theories/Reals/RiemannInt.v @@ -7,7 +7,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: RiemannInt.v 13323 2010-07-24 15:57:30Z herbelin $ i*) Require Import Rfunctions. Require Import SeqSeries. diff --git a/theories/Reals/RiemannInt_SF.v b/theories/Reals/RiemannInt_SF.v index cfb991f9..976050f7 100644 --- a/theories/Reals/RiemannInt_SF.v +++ b/theories/Reals/RiemannInt_SF.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: RiemannInt_SF.v 13323 2010-07-24 15:57:30Z herbelin $ i*) Require Import Rbase. Require Import Rfunctions. diff --git a/theories/Reals/Rlimit.v b/theories/Reals/Rlimit.v index d2a65f42..72aa9971 100644 --- a/theories/Reals/Rlimit.v +++ b/theories/Reals/Rlimit.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: Rlimit.v 13323 2010-07-24 15:57:30Z herbelin $ i*) (*********************************************************) (** Definition of the limit *) diff --git a/theories/Reals/Rpow_def.v b/theories/Reals/Rpow_def.v index e8f034b6..60fc4ca9 100644 --- a/theories/Reals/Rpow_def.v +++ b/theories/Reals/Rpow_def.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) +(* $Id: Rpow_def.v 13323 2010-07-24 15:57:30Z herbelin $ *) Require Import Rdefinitions. diff --git a/theories/Reals/Rpower.v b/theories/Reals/Rpower.v index 35c90d24..4c3a04f6 100644 --- a/theories/Reals/Rpower.v +++ b/theories/Reals/Rpower.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: Rpower.v 13323 2010-07-24 15:57:30Z herbelin $ i*) (*i Due to L.Thery i*) (************************************************************) diff --git a/theories/Reals/Rprod.v b/theories/Reals/Rprod.v index 30b62643..e4269eb7 100644 --- a/theories/Reals/Rprod.v +++ b/theories/Reals/Rprod.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: Rprod.v 13323 2010-07-24 15:57:30Z herbelin $ i*) Require Import Compare. Require Import Rbase. diff --git a/theories/Reals/Rseries.v b/theories/Reals/Rseries.v index 646b2bc0..f7e05fce 100644 --- a/theories/Reals/Rseries.v +++ b/theories/Reals/Rseries.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: Rseries.v 13323 2010-07-24 15:57:30Z herbelin $ i*) Require Import Rbase. Require Import Rfunctions. diff --git a/theories/Reals/Rsigma.v b/theories/Reals/Rsigma.v index 54a13e78..4cfca607 100644 --- a/theories/Reals/Rsigma.v +++ b/theories/Reals/Rsigma.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: Rsigma.v 13323 2010-07-24 15:57:30Z herbelin $ i*) Require Import Rbase. Require Import Rfunctions. diff --git a/theories/Reals/Rsqrt_def.v b/theories/Reals/Rsqrt_def.v index 4c2b423e..9f606fe3 100644 --- a/theories/Reals/Rsqrt_def.v +++ b/theories/Reals/Rsqrt_def.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: Rsqrt_def.v 13323 2010-07-24 15:57:30Z herbelin $ i*) Require Import Sumbool. Require Import Rbase. diff --git a/theories/Reals/Rtopology.v b/theories/Reals/Rtopology.v index b37de502..9b332eea 100644 --- a/theories/Reals/Rtopology.v +++ b/theories/Reals/Rtopology.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: Rtopology.v 13323 2010-07-24 15:57:30Z herbelin $ i*) Require Import Rbase. Require Import Rfunctions. diff --git a/theories/Reals/Rtrigo.v b/theories/Reals/Rtrigo.v index 46914093..bdbea3a6 100644 --- a/theories/Reals/Rtrigo.v +++ b/theories/Reals/Rtrigo.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: Rtrigo.v 13323 2010-07-24 15:57:30Z herbelin $ i*) Require Import Rbase. Require Import Rfunctions. diff --git a/theories/Reals/Rtrigo_alt.v b/theories/Reals/Rtrigo_alt.v index d485ad29..9718d20d 100644 --- a/theories/Reals/Rtrigo_alt.v +++ b/theories/Reals/Rtrigo_alt.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: Rtrigo_alt.v 13323 2010-07-24 15:57:30Z herbelin $ i*) Require Import Rbase. Require Import Rfunctions. diff --git a/theories/Reals/Rtrigo_calc.v b/theories/Reals/Rtrigo_calc.v index b1d47191..9fd7d37c 100644 --- a/theories/Reals/Rtrigo_calc.v +++ b/theories/Reals/Rtrigo_calc.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: Rtrigo_calc.v 13323 2010-07-24 15:57:30Z herbelin $ i*) Require Import Rbase. Require Import Rfunctions. diff --git a/theories/Reals/Rtrigo_def.v b/theories/Reals/Rtrigo_def.v index eb1347a2..b3c4ca23 100644 --- a/theories/Reals/Rtrigo_def.v +++ b/theories/Reals/Rtrigo_def.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: Rtrigo_def.v 13323 2010-07-24 15:57:30Z herbelin $ i*) Require Import Rbase. Require Import Rfunctions. diff --git a/theories/Reals/Rtrigo_fun.v b/theories/Reals/Rtrigo_fun.v index e3338c44..2cb5eadd 100644 --- a/theories/Reals/Rtrigo_fun.v +++ b/theories/Reals/Rtrigo_fun.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: Rtrigo_fun.v 13323 2010-07-24 15:57:30Z herbelin $ i*) Require Import Rbase. Require Import Rfunctions. diff --git a/theories/Reals/Rtrigo_reg.v b/theories/Reals/Rtrigo_reg.v index c5ac16ac..7e771444 100644 --- a/theories/Reals/Rtrigo_reg.v +++ b/theories/Reals/Rtrigo_reg.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: Rtrigo_reg.v 13323 2010-07-24 15:57:30Z herbelin $ i*) Require Import Rbase. Require Import Rfunctions. diff --git a/theories/Reals/SeqProp.v b/theories/Reals/SeqProp.v index 0dcb5ccf..f984dc9c 100644 --- a/theories/Reals/SeqProp.v +++ b/theories/Reals/SeqProp.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: SeqProp.v 13323 2010-07-24 15:57:30Z herbelin $ i*) Require Import Rbase. Require Import Rfunctions. diff --git a/theories/Reals/SeqSeries.v b/theories/Reals/SeqSeries.v index e13c366e..35320589 100644 --- a/theories/Reals/SeqSeries.v +++ b/theories/Reals/SeqSeries.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: SeqSeries.v 13323 2010-07-24 15:57:30Z herbelin $ i*) Require Import Rbase. Require Import Rfunctions. diff --git a/theories/Reals/SplitAbsolu.v b/theories/Reals/SplitAbsolu.v index 06768612..cf050684 100644 --- a/theories/Reals/SplitAbsolu.v +++ b/theories/Reals/SplitAbsolu.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: SplitAbsolu.v 13323 2010-07-24 15:57:30Z herbelin $ i*) Require Import Rbasic_fun. diff --git a/theories/Reals/SplitRmult.v b/theories/Reals/SplitRmult.v index 7ad0dedc..6eb10370 100644 --- a/theories/Reals/SplitRmult.v +++ b/theories/Reals/SplitRmult.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: SplitRmult.v 13323 2010-07-24 15:57:30Z herbelin $ i*) (*i Lemma mult_non_zero :(r1,r2:R)``r1<>0`` /\ ``r2<>0`` -> ``r1*r2<>0``. i*) diff --git a/theories/Reals/Sqrt_reg.v b/theories/Reals/Sqrt_reg.v index 2f897e73..9eea1c53 100644 --- a/theories/Reals/Sqrt_reg.v +++ b/theories/Reals/Sqrt_reg.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: Sqrt_reg.v 13323 2010-07-24 15:57:30Z herbelin $ i*) Require Import Rbase. Require Import Rfunctions. diff --git a/theories/Relations/Operators_Properties.v b/theories/Relations/Operators_Properties.v index a2f4771e..ab431878 100644 --- a/theories/Relations/Operators_Properties.v +++ b/theories/Relations/Operators_Properties.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: Operators_Properties.v 13323 2010-07-24 15:57:30Z herbelin $ i*) (************************************************************************) (** * Some properties of the operators on relations *) diff --git a/theories/Relations/Relation_Definitions.v b/theories/Relations/Relation_Definitions.v index 48e65a1d..71338aa5 100644 --- a/theories/Relations/Relation_Definitions.v +++ b/theories/Relations/Relation_Definitions.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: Relation_Definitions.v 13323 2010-07-24 15:57:30Z herbelin $ i*) Section Relation_Definition. diff --git a/theories/Relations/Relation_Operators.v b/theories/Relations/Relation_Operators.v index a4e4b3e6..8aba6275 100644 --- a/theories/Relations/Relation_Operators.v +++ b/theories/Relations/Relation_Operators.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: Relation_Operators.v 13323 2010-07-24 15:57:30Z herbelin $ i*) (************************************************************************) (** * Bruno Barras, Cristina Cornes *) diff --git a/theories/Relations/Relations.v b/theories/Relations/Relations.v index 22d17493..f98db89b 100644 --- a/theories/Relations/Relations.v +++ b/theories/Relations/Relations.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: Relations.v 13323 2010-07-24 15:57:30Z herbelin $ i*) Require Export Relation_Definitions. Require Export Relation_Operators. diff --git a/theories/Setoids/Setoid.v b/theories/Setoids/Setoid.v index 3262c7ef..8afaedd6 100644 --- a/theories/Setoids/Setoid.v +++ b/theories/Setoids/Setoid.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$: i*) +(*i $Id: Setoid.v 13323 2010-07-24 15:57:30Z herbelin $: i*) Require Export Coq.Classes.SetoidTactics. diff --git a/theories/Sets/Classical_sets.v b/theories/Sets/Classical_sets.v index 824fd036..b20423e0 100644 --- a/theories/Sets/Classical_sets.v +++ b/theories/Sets/Classical_sets.v @@ -24,7 +24,7 @@ (* in Summer 1995. Several developments by E. Ledinot were an inspiration. *) (****************************************************************************) -(*i $Id$ i*) +(*i $Id: Classical_sets.v 13323 2010-07-24 15:57:30Z herbelin $ i*) Require Export Ensembles. Require Export Constructive_sets. diff --git a/theories/Sets/Constructive_sets.v b/theories/Sets/Constructive_sets.v index 8e0ab3b0..bb7235ff 100644 --- a/theories/Sets/Constructive_sets.v +++ b/theories/Sets/Constructive_sets.v @@ -24,7 +24,7 @@ (* in Summer 1995. Several developments by E. Ledinot were an inspiration. *) (****************************************************************************) -(*i $Id$ i*) +(*i $Id: Constructive_sets.v 13323 2010-07-24 15:57:30Z herbelin $ i*) Require Export Ensembles. diff --git a/theories/Sets/Cpo.v b/theories/Sets/Cpo.v index 0781781a..8591aef1 100644 --- a/theories/Sets/Cpo.v +++ b/theories/Sets/Cpo.v @@ -24,7 +24,7 @@ (* in Summer 1995. Several developments by E. Ledinot were an inspiration. *) (****************************************************************************) -(*i $Id$ i*) +(*i $Id: Cpo.v 13323 2010-07-24 15:57:30Z herbelin $ i*) Require Export Ensembles. Require Export Relations_1. diff --git a/theories/Sets/Ensembles.v b/theories/Sets/Ensembles.v index c96c21b4..1fee462d 100644 --- a/theories/Sets/Ensembles.v +++ b/theories/Sets/Ensembles.v @@ -24,7 +24,7 @@ (* in Summer 1995. Several developments by E. Ledinot were an inspiration. *) (****************************************************************************) -(*i $Id$ i*) +(*i $Id: Ensembles.v 13323 2010-07-24 15:57:30Z herbelin $ i*) Section Ensembles. Variable U : Type. diff --git a/theories/Sets/Finite_sets.v b/theories/Sets/Finite_sets.v index cad440b4..f690e894 100644 --- a/theories/Sets/Finite_sets.v +++ b/theories/Sets/Finite_sets.v @@ -24,7 +24,7 @@ (* in Summer 1995. Several developments by E. Ledinot were an inspiration. *) (****************************************************************************) -(*i $Id$ i*) +(*i $Id: Finite_sets.v 13323 2010-07-24 15:57:30Z herbelin $ i*) Require Import Ensembles. diff --git a/theories/Sets/Finite_sets_facts.v b/theories/Sets/Finite_sets_facts.v index cc41a2ea..d351cc74 100644 --- a/theories/Sets/Finite_sets_facts.v +++ b/theories/Sets/Finite_sets_facts.v @@ -24,7 +24,7 @@ (* in Summer 1995. Several developments by E. Ledinot were an inspiration. *) (****************************************************************************) -(*i $Id$ i*) +(*i $Id: Finite_sets_facts.v 13323 2010-07-24 15:57:30Z herbelin $ i*) Require Export Finite_sets. Require Export Constructive_sets. diff --git a/theories/Sets/Image.v b/theories/Sets/Image.v index c48c844c..a58e12e6 100644 --- a/theories/Sets/Image.v +++ b/theories/Sets/Image.v @@ -24,7 +24,7 @@ (* in Summer 1995. Several developments by E. Ledinot were an inspiration. *) (****************************************************************************) -(*i $Id$ i*) +(*i $Id: Image.v 13323 2010-07-24 15:57:30Z herbelin $ i*) Require Export Finite_sets. Require Export Constructive_sets. diff --git a/theories/Sets/Infinite_sets.v b/theories/Sets/Infinite_sets.v index 210205ed..c85cd8d2 100644 --- a/theories/Sets/Infinite_sets.v +++ b/theories/Sets/Infinite_sets.v @@ -24,7 +24,7 @@ (* in Summer 1995. Several developments by E. Ledinot were an inspiration. *) (****************************************************************************) -(*i $Id$ i*) +(*i $Id: Infinite_sets.v 13323 2010-07-24 15:57:30Z herbelin $ i*) Require Export Finite_sets. Require Export Constructive_sets. diff --git a/theories/Sets/Integers.v b/theories/Sets/Integers.v index 29208d03..37173094 100644 --- a/theories/Sets/Integers.v +++ b/theories/Sets/Integers.v @@ -24,7 +24,7 @@ (* in Summer 1995. Several developments by E. Ledinot were an inspiration. *) (****************************************************************************) -(*i $Id$ i*) +(*i $Id: Integers.v 13323 2010-07-24 15:57:30Z herbelin $ i*) Require Export Finite_sets. Require Export Constructive_sets. diff --git a/theories/Sets/Multiset.v b/theories/Sets/Multiset.v index 07fe2721..685a680f 100644 --- a/theories/Sets/Multiset.v +++ b/theories/Sets/Multiset.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: Multiset.v 13323 2010-07-24 15:57:30Z herbelin $ i*) (* G. Huet 1-9-95 *) diff --git a/theories/Sets/Partial_Order.v b/theories/Sets/Partial_Order.v index 95eb5102..671c9690 100644 --- a/theories/Sets/Partial_Order.v +++ b/theories/Sets/Partial_Order.v @@ -24,7 +24,7 @@ (* in Summer 1995. Several developments by E. Ledinot were an inspiration. *) (****************************************************************************) -(*i $Id$ i*) +(*i $Id: Partial_Order.v 13323 2010-07-24 15:57:30Z herbelin $ i*) Require Export Ensembles. Require Export Relations_1. diff --git a/theories/Sets/Permut.v b/theories/Sets/Permut.v index e1caff4f..844989c0 100644 --- a/theories/Sets/Permut.v +++ b/theories/Sets/Permut.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: Permut.v 13323 2010-07-24 15:57:30Z herbelin $ i*) (* G. Huet 1-9-95 *) diff --git a/theories/Sets/Powerset.v b/theories/Sets/Powerset.v index b6df89f3..ae9dbb43 100644 --- a/theories/Sets/Powerset.v +++ b/theories/Sets/Powerset.v @@ -24,7 +24,7 @@ (* in Summer 1995. Several developments by E. Ledinot were an inspiration. *) (****************************************************************************) -(*i $Id$ i*) +(*i $Id: Powerset.v 13323 2010-07-24 15:57:30Z herbelin $ i*) Require Export Ensembles. Require Export Relations_1. diff --git a/theories/Sets/Powerset_Classical_facts.v b/theories/Sets/Powerset_Classical_facts.v index 93cb653a..f9da4816 100644 --- a/theories/Sets/Powerset_Classical_facts.v +++ b/theories/Sets/Powerset_Classical_facts.v @@ -24,7 +24,7 @@ (* in Summer 1995. Several developments by E. Ledinot were an inspiration. *) (****************************************************************************) -(*i $Id$ i*) +(*i $Id: Powerset_Classical_facts.v 13323 2010-07-24 15:57:30Z herbelin $ i*) Require Export Ensembles. Require Export Constructive_sets. diff --git a/theories/Sets/Powerset_facts.v b/theories/Sets/Powerset_facts.v index 7186881a..ab5bbaf9 100644 --- a/theories/Sets/Powerset_facts.v +++ b/theories/Sets/Powerset_facts.v @@ -24,7 +24,7 @@ (* in Summer 1995. Several developments by E. Ledinot were an inspiration. *) (****************************************************************************) -(*i $Id$ i*) +(*i $Id: Powerset_facts.v 13323 2010-07-24 15:57:30Z herbelin $ i*) Require Export Ensembles. Require Export Constructive_sets. diff --git a/theories/Sets/Relations_1.v b/theories/Sets/Relations_1.v index 54a5bd01..4677219e 100644 --- a/theories/Sets/Relations_1.v +++ b/theories/Sets/Relations_1.v @@ -24,7 +24,7 @@ (* in Summer 1995. Several developments by E. Ledinot were an inspiration. *) (****************************************************************************) -(*i $Id$ i*) +(*i $Id: Relations_1.v 13323 2010-07-24 15:57:30Z herbelin $ i*) Section Relations_1. Variable U : Type. diff --git a/theories/Sets/Relations_1_facts.v b/theories/Sets/Relations_1_facts.v index a8d8209b..b6c0df25 100644 --- a/theories/Sets/Relations_1_facts.v +++ b/theories/Sets/Relations_1_facts.v @@ -24,7 +24,7 @@ (* in Summer 1995. Several developments by E. Ledinot were an inspiration. *) (****************************************************************************) -(*i $Id$ i*) +(*i $Id: Relations_1_facts.v 13323 2010-07-24 15:57:30Z herbelin $ i*) Require Export Relations_1. diff --git a/theories/Sets/Relations_2.v b/theories/Sets/Relations_2.v index e9cba979..9f7c831c 100644 --- a/theories/Sets/Relations_2.v +++ b/theories/Sets/Relations_2.v @@ -24,7 +24,7 @@ (* in Summer 1995. Several developments by E. Ledinot were an inspiration. *) (****************************************************************************) -(*i $Id$ i*) +(*i $Id: Relations_2.v 13323 2010-07-24 15:57:30Z herbelin $ i*) Require Export Relations_1. diff --git a/theories/Sets/Relations_2_facts.v b/theories/Sets/Relations_2_facts.v index cbd596c3..039bae87 100644 --- a/theories/Sets/Relations_2_facts.v +++ b/theories/Sets/Relations_2_facts.v @@ -24,7 +24,7 @@ (* in Summer 1995. Several developments by E. Ledinot were an inspiration. *) (****************************************************************************) -(*i $Id$ i*) +(*i $Id: Relations_2_facts.v 13323 2010-07-24 15:57:30Z herbelin $ i*) Require Export Relations_1. Require Export Relations_1_facts. diff --git a/theories/Sets/Relations_3.v b/theories/Sets/Relations_3.v index 99a68efc..d4a3d87c 100644 --- a/theories/Sets/Relations_3.v +++ b/theories/Sets/Relations_3.v @@ -24,7 +24,7 @@ (* in Summer 1995. Several developments by E. Ledinot were an inspiration. *) (****************************************************************************) -(*i $Id$ i*) +(*i $Id: Relations_3.v 13323 2010-07-24 15:57:30Z herbelin $ i*) Require Export Relations_1. Require Export Relations_2. diff --git a/theories/Sets/Relations_3_facts.v b/theories/Sets/Relations_3_facts.v index f85128ae..1a22aff9 100644 --- a/theories/Sets/Relations_3_facts.v +++ b/theories/Sets/Relations_3_facts.v @@ -24,7 +24,7 @@ (* in Summer 1995. Several developments by E. Ledinot were an inspiration. *) (****************************************************************************) -(*i $Id$ i*) +(*i $Id: Relations_3_facts.v 13323 2010-07-24 15:57:30Z herbelin $ i*) Require Export Relations_1. Require Export Relations_1_facts. diff --git a/theories/Sets/Uniset.v b/theories/Sets/Uniset.v index 9803edc8..78da067d 100644 --- a/theories/Sets/Uniset.v +++ b/theories/Sets/Uniset.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: Uniset.v 13323 2010-07-24 15:57:30Z herbelin $ i*) (** Sets as characteristic functions *) diff --git a/theories/Sorting/Heap.v b/theories/Sorting/Heap.v index 2e463120..eb53f061 100644 --- a/theories/Sorting/Heap.v +++ b/theories/Sorting/Heap.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: Heap.v 13346 2010-07-28 17:17:32Z msozeau $ i*) (** This file is deprecated, for a tree on list, use [Mergesort.v]. *) @@ -136,45 +136,46 @@ Section defs. (munion (list_contents _ eqA_dec l1) (list_contents _ eqA_dec l2)) -> (forall a, HdRel leA a l1 -> HdRel leA a l2 -> HdRel leA a l) -> merge_lem l1 l2. - + Require Import Morphisms. + + Instance: Equivalence (@meq A). + Proof. constructor; auto with datatypes. red. apply meq_trans. Defined. + + Instance: Proper (@meq A ++> @meq _ ++> @meq _) (@munion A). + Proof. intros x y H x' y' H'. now apply meq_congr. Qed. + Lemma merge : forall l1:list A, Sorted leA l1 -> forall l2:list A, Sorted leA l2 -> merge_lem l1 l2. Proof. - simple induction 1; intros. + fix 1; intros; destruct l1. apply merge_exist with l2; auto with datatypes. - elim H2; intros. - apply merge_exist with (a :: l); simpl in |- *; auto using cons_sort with datatypes. + rename l1 into l. + revert l2 H0. fix 1. intros. + destruct l2 as [|a0 l0]. + apply merge_exist with (a :: l); simpl; auto with datatypes. elim (leA_dec a a0); intros. (* 1 (leA a a0) *) - cut (merge_lem l (a0 :: l0)); auto using cons_sort with datatypes. - intros [l3 l3sorted l3contents Hrec]. - apply merge_exist with (a :: l3); simpl in |- *; + apply Sorted_inv in H. destruct H. + destruct (merge l H (a0 :: l0) H0). + apply merge_exist with (a :: l1). clear merge merge0. auto using cons_sort, cons_leA with datatypes. - apply meq_trans with - (munion (singletonBag a) - (munion (list_contents _ eqA_dec l) - (list_contents _ eqA_dec (a0 :: l0)))). - apply meq_right; trivial with datatypes. - apply meq_sym; apply munion_ass. - intros; apply cons_leA. + simpl. rewrite m. now rewrite munion_ass. + intros. apply cons_leA. apply (@HdRel_inv _ leA) with l; trivial with datatypes. (* 2 (leA a0 a) *) - elim X0; simpl in |- *; intros. - apply merge_exist with (a0 :: l3); simpl in |- *; + apply Sorted_inv in H0. destruct H0. + destruct (merge0 l0 H0). clear merge merge0. + apply merge_exist with (a0 :: l1); auto using cons_sort, cons_leA with datatypes. - apply meq_trans with - (munion (singletonBag a0) - (munion (munion (singletonBag a) (list_contents _ eqA_dec l)) - (list_contents _ eqA_dec l0))). - apply meq_right; trivial with datatypes. - apply munion_perm_left. - intros; apply cons_leA; apply HdRel_inv with (l:=l0); trivial with datatypes. + simpl; rewrite m. simpl. setoid_rewrite munion_ass at 1. rewrite munion_comm. + repeat rewrite munion_ass. setoid_rewrite munion_comm at 3. reflexivity. + intros. apply cons_leA. + apply (@HdRel_inv _ leA) with l0; trivial with datatypes. Qed. - (** ** From trees to multisets *) (** contents of a tree as a multiset *) diff --git a/theories/Sorting/Mergesort.v b/theories/Sorting/Mergesort.v index f52a24b4..e576db2b 100644 --- a/theories/Sorting/Mergesort.v +++ b/theories/Sorting/Mergesort.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: Mergesort.v 13323 2010-07-24 15:57:30Z herbelin $ i*) (** A modular implementation of mergesort (the complexity is O(n.log n) in the length of the list) *) diff --git a/theories/Sorting/PermutEq.v b/theories/Sorting/PermutEq.v index 1388df6a..00a09051 100644 --- a/theories/Sorting/PermutEq.v +++ b/theories/Sorting/PermutEq.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: PermutEq.v 13323 2010-07-24 15:57:30Z herbelin $ i*) Require Import Relations Setoid SetoidList List Multiset PermutSetoid Permutation. diff --git a/theories/Sorting/PermutSetoid.v b/theories/Sorting/PermutSetoid.v index f5f91887..e47e2b84 100644 --- a/theories/Sorting/PermutSetoid.v +++ b/theories/Sorting/PermutSetoid.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: PermutSetoid.v 13323 2010-07-24 15:57:30Z herbelin $ i*) Require Import Omega Relations Multiset SetoidList. diff --git a/theories/Sorting/Permutation.v b/theories/Sorting/Permutation.v index f88c29cb..1e145f57 100644 --- a/theories/Sorting/Permutation.v +++ b/theories/Sorting/Permutation.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: Permutation.v 13323 2010-07-24 15:57:30Z herbelin $ i*) (*********************************************************************) (** ** List permutations as a composition of adjacent transpositions *) diff --git a/theories/Sorting/Sorted.v b/theories/Sorting/Sorted.v index 7d75d60a..ab399d40 100644 --- a/theories/Sorting/Sorted.v +++ b/theories/Sorting/Sorted.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: Sorted.v 13323 2010-07-24 15:57:30Z herbelin $ i*) (* Made by Hugo Herbelin *) diff --git a/theories/Sorting/Sorting.v b/theories/Sorting/Sorting.v index 85d89441..860e0517 100644 --- a/theories/Sorting/Sorting.v +++ b/theories/Sorting/Sorting.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: Sorting.v 13323 2010-07-24 15:57:30Z herbelin $ i*) Require Export Sorted. Require Export Mergesort. diff --git a/theories/Strings/Ascii.v b/theories/Strings/Ascii.v index de1684b4..31a18f25 100644 --- a/theories/Strings/Ascii.v +++ b/theories/Strings/Ascii.v @@ -7,7 +7,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) +(* $Id: Ascii.v 13323 2010-07-24 15:57:30Z herbelin $ *) (** Contributed by Laurent Théry (INRIA); Adapted to Coq V8 by the Coq Development Team *) diff --git a/theories/Strings/String.v b/theories/Strings/String.v index c2d59679..4b7c1c2d 100644 --- a/theories/Strings/String.v +++ b/theories/Strings/String.v @@ -7,7 +7,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) +(* $Id: String.v 13323 2010-07-24 15:57:30Z herbelin $ *) (** Contributed by Laurent Théry (INRIA); Adapted to Coq V8 by the Coq Development Team *) diff --git a/theories/Structures/DecidableType.v b/theories/Structures/DecidableType.v index 2c72e30b..18153436 100644 --- a/theories/Structures/DecidableType.v +++ b/theories/Structures/DecidableType.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -(* $Id$ *) +(* $Id: DecidableType.v 12641 2010-01-07 15:32:52Z letouzey $ *) Require Export SetoidList. Require Equalities. diff --git a/theories/Structures/DecidableTypeEx.v b/theories/Structures/DecidableTypeEx.v index 4407ead4..ac1f014b 100644 --- a/theories/Structures/DecidableTypeEx.v +++ b/theories/Structures/DecidableTypeEx.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -(* $Id$ *) +(* $Id: DecidableTypeEx.v 12641 2010-01-07 15:32:52Z letouzey $ *) Require Import DecidableType OrderedType OrderedTypeEx. Set Implicit Arguments. diff --git a/theories/Structures/Equalities.v b/theories/Structures/Equalities.v index 487b1d0c..d205c0e0 100644 --- a/theories/Structures/Equalities.v +++ b/theories/Structures/Equalities.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -(* $Id$ *) +(* $Id: Equalities.v 12662 2010-01-13 16:53:01Z letouzey $ *) Require Export RelationClasses. diff --git a/theories/Structures/OrderedType.v b/theories/Structures/OrderedType.v index 72fbe796..57f491d2 100644 --- a/theories/Structures/OrderedType.v +++ b/theories/Structures/OrderedType.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -(* $Id$ *) +(* $Id: OrderedType.v 12732 2010-02-10 22:46:59Z letouzey $ *) Require Export SetoidList Morphisms OrdersTac. Set Implicit Arguments. diff --git a/theories/Structures/OrderedTypeAlt.v b/theories/Structures/OrderedTypeAlt.v index 23ae4c85..f6c1532b 100644 --- a/theories/Structures/OrderedTypeAlt.v +++ b/theories/Structures/OrderedTypeAlt.v @@ -5,7 +5,7 @@ (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -(* $Id$ *) +(* $Id: OrderedTypeAlt.v 12384 2009-10-13 14:39:51Z letouzey $ *) Require Import OrderedType. diff --git a/theories/Structures/OrderedTypeEx.v b/theories/Structures/OrderedTypeEx.v index b4dbceba..128cd576 100644 --- a/theories/Structures/OrderedTypeEx.v +++ b/theories/Structures/OrderedTypeEx.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -(* $Id$ *) +(* $Id: OrderedTypeEx.v 13297 2010-07-19 23:32:42Z letouzey $ *) Require Import OrderedType. Require Import ZArith. diff --git a/theories/Structures/Orders.v b/theories/Structures/Orders.v index bddd461a..5567b743 100644 --- a/theories/Structures/Orders.v +++ b/theories/Structures/Orders.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -(* $Id$ *) +(* $Id: Orders.v 13276 2010-07-10 14:34:44Z letouzey $ *) Require Export Relations Morphisms Setoid Equalities. Set Implicit Arguments. diff --git a/theories/Structures/OrdersAlt.v b/theories/Structures/OrdersAlt.v index d86b02a1..21ef8eb8 100644 --- a/theories/Structures/OrdersAlt.v +++ b/theories/Structures/OrdersAlt.v @@ -11,7 +11,7 @@ * Institution: LRI, CNRS UMR 8623 - Université Paris Sud * 91405 Orsay, France *) -(* $Id$ *) +(* $Id: OrdersAlt.v 12754 2010-02-12 16:21:48Z letouzey $ *) Require Import OrderedType Orders. Set Implicit Arguments. diff --git a/theories/Structures/OrdersEx.v b/theories/Structures/OrdersEx.v index 56f1d5de..9f83d82b 100644 --- a/theories/Structures/OrdersEx.v +++ b/theories/Structures/OrdersEx.v @@ -11,7 +11,7 @@ * Institution: LRI, CNRS UMR 8623 - Université Paris Sud * 91405 Orsay, France *) -(* $Id$ *) +(* $Id: OrdersEx.v 12641 2010-01-07 15:32:52Z letouzey $ *) Require Import Orders NatOrderedType POrderedType NOrderedType ZOrderedType RelationPairs EqualitiesFacts. diff --git a/theories/Unicode/Utf8_core.v b/theories/Unicode/Utf8_core.v new file mode 100644 index 00000000..a42de3ab --- /dev/null +++ b/theories/Unicode/Utf8_core.v @@ -0,0 +1,25 @@ +(* -*- coding:utf-8 -*- *) +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* Logic *) +Notation "∀ x .. y , P" := (forall x, .. (forall y, P) ..) + (at level 200, x binder, y binder, right associativity) : type_scope. +Notation "∃ x .. y , P" := (exists x, .. (exists y, P) ..) + (at level 200, x binder, y binder, right associativity) : type_scope. + +Notation "x ∨ y" := (x \/ y) (at level 85, right associativity) : type_scope. +Notation "x ∧ y" := (x /\ y) (at level 80, right associativity) : type_scope. +Notation "x → y" := (x -> y) (at level 90, right associativity): type_scope. +Notation "x ↔ y" := (x <-> y) (at level 95, no associativity): type_scope. +Notation "¬ x" := (~x) (at level 75, right associativity) : type_scope. +Notation "x ≠ y" := (x <> y) (at level 70) : type_scope. + +(* Abstraction *) +Notation "'λ' x .. y , t" := (fun x => .. (fun y => t) ..) + (at level 200, x binder, y binder, right associativity). diff --git a/theories/Unicode/vo.itarget b/theories/Unicode/vo.itarget index 243a40b7..7be1b996 100644 --- a/theories/Unicode/vo.itarget +++ b/theories/Unicode/vo.itarget @@ -1 +1,2 @@ Utf8.vo +Utf8_core.vo diff --git a/theories/Wellfounded/Disjoint_Union.v b/theories/Wellfounded/Disjoint_Union.v index 30041b86..7fbddb9e 100644 --- a/theories/Wellfounded/Disjoint_Union.v +++ b/theories/Wellfounded/Disjoint_Union.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: Disjoint_Union.v 13323 2010-07-24 15:57:30Z herbelin $ i*) (** Author: Cristina Cornes From : Constructing Recursion Operators in Type Theory diff --git a/theories/Wellfounded/Inclusion.v b/theories/Wellfounded/Inclusion.v index 80b2e73c..0a72a77a 100644 --- a/theories/Wellfounded/Inclusion.v +++ b/theories/Wellfounded/Inclusion.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: Inclusion.v 13323 2010-07-24 15:57:30Z herbelin $ i*) (** Author: Bruno Barras *) diff --git a/theories/Wellfounded/Inverse_Image.v b/theories/Wellfounded/Inverse_Image.v index 762d26a9..6aa7a878 100644 --- a/theories/Wellfounded/Inverse_Image.v +++ b/theories/Wellfounded/Inverse_Image.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: Inverse_Image.v 13323 2010-07-24 15:57:30Z herbelin $ i*) (** Author: Bruno Barras *) diff --git a/theories/Wellfounded/Lexicographic_Exponentiation.v b/theories/Wellfounded/Lexicographic_Exponentiation.v index f27746c8..db7b106f 100644 --- a/theories/Wellfounded/Lexicographic_Exponentiation.v +++ b/theories/Wellfounded/Lexicographic_Exponentiation.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: Lexicographic_Exponentiation.v 13323 2010-07-24 15:57:30Z herbelin $ i*) (** Author: Cristina Cornes diff --git a/theories/Wellfounded/Lexicographic_Product.v b/theories/Wellfounded/Lexicographic_Product.v index 8a955c34..29fabbc2 100644 --- a/theories/Wellfounded/Lexicographic_Product.v +++ b/theories/Wellfounded/Lexicographic_Product.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: Lexicographic_Product.v 13323 2010-07-24 15:57:30Z herbelin $ i*) (** Authors: Bruno Barras, Cristina Cornes *) diff --git a/theories/Wellfounded/Transitive_Closure.v b/theories/Wellfounded/Transitive_Closure.v index 7c373495..c5cd239a 100644 --- a/theories/Wellfounded/Transitive_Closure.v +++ b/theories/Wellfounded/Transitive_Closure.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: Transitive_Closure.v 13323 2010-07-24 15:57:30Z herbelin $ i*) (** Author: Bruno Barras *) diff --git a/theories/Wellfounded/Union.v b/theories/Wellfounded/Union.v index 50777a3e..3bc7470f 100644 --- a/theories/Wellfounded/Union.v +++ b/theories/Wellfounded/Union.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: Union.v 13323 2010-07-24 15:57:30Z herbelin $ i*) (** Author: Bruno Barras *) diff --git a/theories/Wellfounded/Well_Ordering.v b/theories/Wellfounded/Well_Ordering.v index 8d298058..0f675cfa 100644 --- a/theories/Wellfounded/Well_Ordering.v +++ b/theories/Wellfounded/Well_Ordering.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: Well_Ordering.v 13323 2010-07-24 15:57:30Z herbelin $ i*) (** Author: Cristina Cornes. From: Constructing Recursion Operators in Type Theory diff --git a/theories/Wellfounded/Wellfounded.v b/theories/Wellfounded/Wellfounded.v index 77d82219..1ab6ac87 100644 --- a/theories/Wellfounded/Wellfounded.v +++ b/theories/Wellfounded/Wellfounded.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: Wellfounded.v 13323 2010-07-24 15:57:30Z herbelin $ i*) Require Export Disjoint_Union. Require Export Inclusion. diff --git a/theories/ZArith/BinInt.v b/theories/ZArith/BinInt.v index 5dbeffa4..2a615311 100644 --- a/theories/ZArith/BinInt.v +++ b/theories/ZArith/BinInt.v @@ -7,7 +7,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: BinInt.v 13323 2010-07-24 15:57:30Z herbelin $ i*) (***********************************************************) (** Binary Integers (Pierre Crégut, CNET, Lannion, France) *) diff --git a/theories/ZArith/Int.v b/theories/ZArith/Int.v index 30c08fdc..c0123ca8 100644 --- a/theories/ZArith/Int.v +++ b/theories/ZArith/Int.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -(* $Id$ *) +(* $Id: Int.v 12363 2009-09-28 15:04:07Z letouzey $ *) (** * An light axiomatization of integers (used in FSetAVL). *) diff --git a/theories/ZArith/Wf_Z.v b/theories/ZArith/Wf_Z.v index f073463f..d449100c 100644 --- a/theories/ZArith/Wf_Z.v +++ b/theories/ZArith/Wf_Z.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: Wf_Z.v 13323 2010-07-24 15:57:30Z herbelin $ i*) Require Import BinInt. Require Import Zcompare. diff --git a/theories/ZArith/ZArith.v b/theories/ZArith/ZArith.v index e3937278..96d42077 100644 --- a/theories/ZArith/ZArith.v +++ b/theories/ZArith/ZArith.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: ZArith.v 13323 2010-07-24 15:57:30Z herbelin $ i*) (** Library for manipulating integers based on binary encoding *) diff --git a/theories/ZArith/ZArith_base.v b/theories/ZArith/ZArith_base.v index 6a60a021..4af8eb8f 100644 --- a/theories/ZArith/ZArith_base.v +++ b/theories/ZArith/ZArith_base.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) +(* $Id: ZArith_base.v 13323 2010-07-24 15:57:30Z herbelin $ *) (** Library for manipulating integers based on binary encoding. These are the basic modules, required by [Omega] and [Ring] for instance. diff --git a/theories/ZArith/ZArith_dec.v b/theories/ZArith/ZArith_dec.v index c4d7cef4..1c5efb07 100644 --- a/theories/ZArith/ZArith_dec.v +++ b/theories/ZArith/ZArith_dec.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: ZArith_dec.v 13323 2010-07-24 15:57:30Z herbelin $ i*) Require Import Sumbool. diff --git a/theories/ZArith/Zabs.v b/theories/ZArith/Zabs.v index 2c1b8e74..0057c29c 100644 --- a/theories/ZArith/Zabs.v +++ b/theories/ZArith/Zabs.v @@ -6,7 +6,7 @@ (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: Zabs.v 13323 2010-07-24 15:57:30Z herbelin $ i*) (** Binary Integers (Pierre Crégut (CNET, Lannion, France) *) diff --git a/theories/ZArith/Zbool.v b/theories/ZArith/Zbool.v index fcc2f5b8..79cef8f9 100644 --- a/theories/ZArith/Zbool.v +++ b/theories/ZArith/Zbool.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) +(* $Id: Zbool.v 13323 2010-07-24 15:57:30Z herbelin $ *) Require Import BinInt. Require Import Zeven. diff --git a/theories/ZArith/Zcomplements.v b/theories/ZArith/Zcomplements.v index d8a5781c..2163e211 100644 --- a/theories/ZArith/Zcomplements.v +++ b/theories/ZArith/Zcomplements.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: Zcomplements.v 13323 2010-07-24 15:57:30Z herbelin $ i*) Require Import ZArithRing. Require Import ZArith_base. diff --git a/theories/ZArith/Zdigits.v b/theories/ZArith/Zdigits.v index 71466e9e..78a78007 100644 --- a/theories/ZArith/Zdigits.v +++ b/theories/ZArith/Zdigits.v @@ -7,7 +7,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: Zdigits.v 13323 2010-07-24 15:57:30Z herbelin $ i*) (** Bit vectors interpreted as integers. Contribution by Jean Duprat (ENS Lyon). *) diff --git a/theories/ZArith/Zdiv.v b/theories/ZArith/Zdiv.v index 78dd7050..0f2268cd 100644 --- a/theories/ZArith/Zdiv.v +++ b/theories/ZArith/Zdiv.v @@ -7,7 +7,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: Zdiv.v 13323 2010-07-24 15:57:30Z herbelin $ i*) (* Contribution by Claude Marché and Xavier Urbain *) diff --git a/theories/ZArith/Zeven.v b/theories/ZArith/Zeven.v index d4fdaca8..3923d8aa 100644 --- a/theories/ZArith/Zeven.v +++ b/theories/ZArith/Zeven.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: Zeven.v 13323 2010-07-24 15:57:30Z herbelin $ i*) Require Import BinInt. diff --git a/theories/ZArith/Zgcd_alt.v b/theories/ZArith/Zgcd_alt.v index e5767ddd..26c3c0c2 100644 --- a/theories/ZArith/Zgcd_alt.v +++ b/theories/ZArith/Zgcd_alt.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: Zgcd_alt.v 13323 2010-07-24 15:57:30Z herbelin $ i*) (** * Zgcd_alt : an alternate version of Zgcd, based on Euler's algorithm *) diff --git a/theories/ZArith/Zhints.v b/theories/ZArith/Zhints.v index f41e2f01..5dd8c23c 100644 --- a/theories/ZArith/Zhints.v +++ b/theories/ZArith/Zhints.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: Zhints.v 13323 2010-07-24 15:57:30Z herbelin $ i*) (** This file centralizes the lemmas about [Z], classifying them according to the way they can be used in automatic search *) diff --git a/theories/ZArith/Zlogarithm.v b/theories/ZArith/Zlogarithm.v index 0666380a..67650b0c 100644 --- a/theories/ZArith/Zlogarithm.v +++ b/theories/ZArith/Zlogarithm.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: Zlogarithm.v 13323 2010-07-24 15:57:30Z herbelin $ i*) (**********************************************************************) (** The integer logarithms with base 2. diff --git a/theories/ZArith/Zmax.v b/theories/ZArith/Zmax.v index 48b9c858..7285ec5a 100644 --- a/theories/ZArith/Zmax.v +++ b/theories/ZArith/Zmax.v @@ -5,7 +5,7 @@ (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: Zmax.v 13323 2010-07-24 15:57:30Z herbelin $ i*) (** THIS FILE IS DEPRECATED. Use [Zminmax] instead. *) diff --git a/theories/ZArith/Zmin.v b/theories/ZArith/Zmin.v index f9b23fde..5b1564d6 100644 --- a/theories/ZArith/Zmin.v +++ b/theories/ZArith/Zmin.v @@ -5,7 +5,7 @@ (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: Zmin.v 13323 2010-07-24 15:57:30Z herbelin $ i*) (** THIS FILE IS DEPRECATED. Use [Zminmax] instead. *) diff --git a/theories/ZArith/Zmisc.v b/theories/ZArith/Zmisc.v index 50d4c7f8..f625f762 100644 --- a/theories/ZArith/Zmisc.v +++ b/theories/ZArith/Zmisc.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: Zmisc.v 13323 2010-07-24 15:57:30Z herbelin $ i*) Require Import Wf_nat. Require Import BinInt. diff --git a/theories/ZArith/Znat.v b/theories/ZArith/Znat.v index cd258af3..0feb4df1 100644 --- a/theories/ZArith/Znat.v +++ b/theories/ZArith/Znat.v @@ -7,7 +7,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: Znat.v 13323 2010-07-24 15:57:30Z herbelin $ i*) (** Binary Integers (Pierre Crégut, CNET, Lannion, France) *) diff --git a/theories/ZArith/Znumtheory.v b/theories/ZArith/Znumtheory.v index 4347d70c..c3394ed4 100644 --- a/theories/ZArith/Znumtheory.v +++ b/theories/ZArith/Znumtheory.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: Znumtheory.v 13323 2010-07-24 15:57:30Z herbelin $ i*) Require Import ZArith_base. Require Import ZArithRing. diff --git a/theories/ZArith/Zorder.v b/theories/ZArith/Zorder.v index 13112e01..a691d269 100644 --- a/theories/ZArith/Zorder.v +++ b/theories/ZArith/Zorder.v @@ -6,7 +6,7 @@ (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: Zorder.v 13323 2010-07-24 15:57:30Z herbelin $ i*) (** Binary Integers (Pierre Crégut, CNET, Lannion, France) *) diff --git a/theories/ZArith/Zpow_facts.v b/theories/ZArith/Zpow_facts.v index 84b49799..226a573c 100644 --- a/theories/ZArith/Zpow_facts.v +++ b/theories/ZArith/Zpow_facts.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: Zpow_facts.v 13323 2010-07-24 15:57:30Z herbelin $ i*) Require Import ZArith_base. Require Import ZArithRing. diff --git a/theories/ZArith/Zpower.v b/theories/ZArith/Zpower.v index 6e30ca08..e7c2fc57 100644 --- a/theories/ZArith/Zpower.v +++ b/theories/ZArith/Zpower.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: Zpower.v 13323 2010-07-24 15:57:30Z herbelin $ i*) Require Import Wf_nat. Require Import ZArith_base. diff --git a/theories/ZArith/Zsqrt.v b/theories/ZArith/Zsqrt.v index 1e9db3d1..8d4f70e9 100644 --- a/theories/ZArith/Zsqrt.v +++ b/theories/ZArith/Zsqrt.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) +(* $Id: Zsqrt.v 13323 2010-07-24 15:57:30Z herbelin $ *) Require Import ZArithRing. Require Import Omega. diff --git a/theories/ZArith/Zwf.v b/theories/ZArith/Zwf.v index 03678a27..cc4687ee 100644 --- a/theories/ZArith/Zwf.v +++ b/theories/ZArith/Zwf.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) +(* $Id: Zwf.v 13323 2010-07-24 15:57:30Z herbelin $ *) Require Import ZArith_base. Require Export Wf_nat. diff --git a/theories/ZArith/auxiliary.v b/theories/ZArith/auxiliary.v index bd2033b8..f50e7bf7 100644 --- a/theories/ZArith/auxiliary.v +++ b/theories/ZArith/auxiliary.v @@ -7,7 +7,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: auxiliary.v 13323 2010-07-24 15:57:30Z herbelin $ i*) (** Binary Integers (Pierre Crégut, CNET, Lannion, France) *) |