diff options
Diffstat (limited to 'theories')
57 files changed, 210 insertions, 130 deletions
diff --git a/theories/Numbers/BigNumPrelude.v b/theories/Numbers/BigNumPrelude.v index 8e4b1d64f..586e50167 100644 --- a/theories/Numbers/BigNumPrelude.v +++ b/theories/Numbers/BigNumPrelude.v @@ -1,16 +1,20 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) +(* Benjamin Gregoire, Laurent Thery, INRIA, 2007 *) +(************************************************************************) -(*************************************************************) -(* This file is distributed under the terms of the *) -(* GNU Lesser General Public License Version 2.1 *) -(*************************************************************) -(* Benjamin.Gregoire@inria.fr Laurent.Thery@inria.fr *) -(*************************************************************) +(*i $Id$ i*) -(********************************************************************** - Aux.v +(** * BigNumPrelude *) + +(** Auxillary functions & theorems used for arbitrary precision efficient + numbers. *) - Auxillary functions & Theorems - **********************************************************************) Require Import ArithRing. Require Export ZArith. diff --git a/theories/Numbers/Cyclic/Abstract/ZnZ.v b/theories/Numbers/Cyclic/Abstract/ZnZ.v index dfe091209..877e49c11 100644 --- a/theories/Numbers/Cyclic/Abstract/ZnZ.v +++ b/theories/Numbers/Cyclic/Abstract/ZnZ.v @@ -5,19 +5,13 @@ (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* Benjamin Gregoire, INRIA Laurent Thery, INRIA *) +(* Benjamin Gregoire, Laurent Thery, INRIA, 2007 *) (************************************************************************) (* $Id$ *) (** * Signature and specification of a bounded integer structure *) -(** -- Authors: Benjamin Grégoire, Laurent Théry -- Institution: INRIA -- Date: 2007 -*) - Set Implicit Arguments. Require Import ZArith. diff --git a/theories/Numbers/Cyclic/DoubleCyclic/Basic_type.v b/theories/Numbers/Cyclic/DoubleCyclic/Basic_type.v index 2116aaddd..60fa09584 100644 --- a/theories/Numbers/Cyclic/DoubleCyclic/Basic_type.v +++ b/theories/Numbers/Cyclic/DoubleCyclic/Basic_type.v @@ -5,13 +5,10 @@ (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +(* Benjamin Gregoire, Laurent Thery, INRIA, 2007 *) +(************************************************************************) -(*************************************************************) -(* This file is distributed under the terms of the *) -(* GNU Lesser General Public License Version 2.1 *) -(*************************************************************) -(* Benjamin.Gregoire@inria.fr Laurent.Thery@inria.fr *) -(*************************************************************) +(*i $Id$ i*) Set Implicit Arguments. diff --git a/theories/Numbers/Cyclic/DoubleCyclic/GenAdd.v b/theories/Numbers/Cyclic/DoubleCyclic/GenAdd.v index 889ccaa4d..68703129b 100644 --- a/theories/Numbers/Cyclic/DoubleCyclic/GenAdd.v +++ b/theories/Numbers/Cyclic/DoubleCyclic/GenAdd.v @@ -5,13 +5,10 @@ (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +(* Benjamin Gregoire, Laurent Thery, INRIA, 2007 *) +(************************************************************************) -(*************************************************************) -(* This file is distributed under the terms of the *) -(* GNU Lesser General Public License Version 2.1 *) -(*************************************************************) -(* Benjamin.Gregoire@inria.fr Laurent.Thery@inria.fr *) -(*************************************************************) +(*i $Id$ i*) Set Implicit Arguments. diff --git a/theories/Numbers/Cyclic/DoubleCyclic/GenBase.v b/theories/Numbers/Cyclic/DoubleCyclic/GenBase.v index 2283e3ca0..eb517c060 100644 --- a/theories/Numbers/Cyclic/DoubleCyclic/GenBase.v +++ b/theories/Numbers/Cyclic/DoubleCyclic/GenBase.v @@ -5,17 +5,10 @@ (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +(* Benjamin Gregoire, Laurent Thery, INRIA, 2007 *) +(************************************************************************) -(* $Id$ *) - -(** * *) - -(** -- Authors: Benjamin Grégoire, Laurent Théry -- Institution: INRIA -- Date: 2007 -- Remark: File automatically generated -*) +(*i $Id$ i*) Set Implicit Arguments. diff --git a/theories/Numbers/Cyclic/DoubleCyclic/GenDiv.v b/theories/Numbers/Cyclic/DoubleCyclic/GenDiv.v index 0e9993b10..057ad3c06 100644 --- a/theories/Numbers/Cyclic/DoubleCyclic/GenDiv.v +++ b/theories/Numbers/Cyclic/DoubleCyclic/GenDiv.v @@ -1,10 +1,14 @@ - -(*************************************************************) -(* This file is distributed under the terms of the *) -(* GNU Lesser General Public License Version 2.1 *) -(*************************************************************) -(* Benjamin.Gregoire@inria.fr Laurent.Thery@inria.fr *) -(*************************************************************) +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) +(* Benjamin Gregoire, Laurent Thery, INRIA, 2007 *) +(************************************************************************) + +(*i $Id$ i*) Set Implicit Arguments. diff --git a/theories/Numbers/Cyclic/DoubleCyclic/GenDivn1.v b/theories/Numbers/Cyclic/DoubleCyclic/GenDivn1.v index a686f0c27..cbf487f4b 100644 --- a/theories/Numbers/Cyclic/DoubleCyclic/GenDivn1.v +++ b/theories/Numbers/Cyclic/DoubleCyclic/GenDivn1.v @@ -1,10 +1,14 @@ - -(*************************************************************) -(* This file is distributed under the terms of the *) -(* GNU Lesser General Public License Version 2.1 *) -(*************************************************************) -(* Benjamin.Gregoire@inria.fr Laurent.Thery@inria.fr *) -(*************************************************************) +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) +(* Benjamin Gregoire, Laurent Thery, INRIA, 2007 *) +(************************************************************************) + +(*i $Id$ i*) Set Implicit Arguments. diff --git a/theories/Numbers/Cyclic/DoubleCyclic/GenLift.v b/theories/Numbers/Cyclic/DoubleCyclic/GenLift.v index 5f8b00a52..6cc1ecad3 100644 --- a/theories/Numbers/Cyclic/DoubleCyclic/GenLift.v +++ b/theories/Numbers/Cyclic/DoubleCyclic/GenLift.v @@ -1,10 +1,14 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) +(* Benjamin Gregoire, Laurent Thery, INRIA, 2007 *) +(************************************************************************) -(*************************************************************) -(* This file is distributed under the terms of the *) -(* GNU Lesser General Public License Version 2.1 *) -(*************************************************************) -(* Benjamin.Gregoire@inria.fr Laurent.Thery@inria.fr *) -(*************************************************************) +(*i $Id$ i*) Set Implicit Arguments. diff --git a/theories/Numbers/Cyclic/DoubleCyclic/GenMul.v b/theories/Numbers/Cyclic/DoubleCyclic/GenMul.v index 57cdeeb88..f42946d6f 100644 --- a/theories/Numbers/Cyclic/DoubleCyclic/GenMul.v +++ b/theories/Numbers/Cyclic/DoubleCyclic/GenMul.v @@ -1,10 +1,14 @@ - -(*************************************************************) -(* This file is distributed under the terms of the *) -(* GNU Lesser General Public License Version 2.1 *) -(*************************************************************) -(* Benjamin.Gregoire@inria.fr Laurent.Thery@inria.fr *) -(*************************************************************) +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) +(* Benjamin Gregoire, Laurent Thery, INRIA, 2007 *) +(************************************************************************) + +(*i $Id$ i*) Set Implicit Arguments. diff --git a/theories/Numbers/Cyclic/DoubleCyclic/GenSqrt.v b/theories/Numbers/Cyclic/DoubleCyclic/GenSqrt.v index f8cb16858..ce312aa62 100644 --- a/theories/Numbers/Cyclic/DoubleCyclic/GenSqrt.v +++ b/theories/Numbers/Cyclic/DoubleCyclic/GenSqrt.v @@ -1,10 +1,14 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) +(* Benjamin Gregoire, Laurent Thery, INRIA, 2007 *) +(************************************************************************) -(*************************************************************) -(* This file is distributed under the terms of the *) -(* GNU Lesser General Public License Version 2.1 *) -(*************************************************************) -(* Benjamin.Gregoire@inria.fr Laurent.Thery@inria.fr *) -(*************************************************************) +(*i $Id$ i*) Set Implicit Arguments. diff --git a/theories/Numbers/Cyclic/DoubleCyclic/GenSub.v b/theories/Numbers/Cyclic/DoubleCyclic/GenSub.v index b96d09562..3babd7716 100644 --- a/theories/Numbers/Cyclic/DoubleCyclic/GenSub.v +++ b/theories/Numbers/Cyclic/DoubleCyclic/GenSub.v @@ -1,10 +1,14 @@ - -(*************************************************************) -(* This file is distributed under the terms of the *) -(* GNU Lesser General Public License Version 2.1 *) -(*************************************************************) -(* Benjamin.Gregoire@inria.fr Laurent.Thery@inria.fr *) -(*************************************************************) +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) +(* Benjamin Gregoire, Laurent Thery, INRIA, 2007 *) +(************************************************************************) + +(*i $Id$ i*) Set Implicit Arguments. diff --git a/theories/Numbers/Cyclic/DoubleCyclic/Zn2Z.v b/theories/Numbers/Cyclic/DoubleCyclic/Zn2Z.v index 9b77cf039..a70f3c8ec 100644 --- a/theories/Numbers/Cyclic/DoubleCyclic/Zn2Z.v +++ b/theories/Numbers/Cyclic/DoubleCyclic/Zn2Z.v @@ -1,10 +1,14 @@ - -(*************************************************************) -(* This file is distributed under the terms of the *) -(* GNU Lesser General Public License Version 2.1 *) -(*************************************************************) -(* Benjamin.Gregoire@inria.fr Laurent.Thery@inria.fr *) -(*************************************************************) +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) +(* Benjamin Gregoire, Laurent Thery, INRIA, 2007 *) +(************************************************************************) + +(*i $Id$ i*) Set Implicit Arguments. diff --git a/theories/Numbers/Cyclic/Int31/Int31.v b/theories/Numbers/Cyclic/Int31/Int31.v index d7e80d4a2..032326c81 100644 --- a/theories/Numbers/Cyclic/Int31/Int31.v +++ b/theories/Numbers/Cyclic/Int31/Int31.v @@ -5,8 +5,10 @@ (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +(* Benjamin Gregoire, Laurent Thery, INRIA, 2007 *) +(************************************************************************) -(*i $ $ i*) +(*i $Id$ i*) (* Require Import Notations.*) Require Export ZArith. diff --git a/theories/Numbers/Integer/Abstract/ZAxioms.v b/theories/Numbers/Integer/Abstract/ZAxioms.v index fdc7bab4c..678781b23 100644 --- a/theories/Numbers/Integer/Abstract/ZAxioms.v +++ b/theories/Numbers/Integer/Abstract/ZAxioms.v @@ -8,7 +8,7 @@ (* Evgeny Makarov, INRIA, 2007 *) (************************************************************************) -(*i i*) +(*i $Id$ i*) Require Export NZAxioms. diff --git a/theories/Numbers/Integer/Abstract/ZBase.v b/theories/Numbers/Integer/Abstract/ZBase.v index 0813a3caa..c57f9ede0 100644 --- a/theories/Numbers/Integer/Abstract/ZBase.v +++ b/theories/Numbers/Integer/Abstract/ZBase.v @@ -8,7 +8,7 @@ (* Evgeny Makarov, INRIA, 2007 *) (************************************************************************) -(*i i*) +(*i $Id$ i*) Require Export Decidable. Require Export ZAxioms. diff --git a/theories/Numbers/Integer/Abstract/ZDomain.v b/theories/Numbers/Integer/Abstract/ZDomain.v index 51b522a52..ce3ca21c2 100644 --- a/theories/Numbers/Integer/Abstract/ZDomain.v +++ b/theories/Numbers/Integer/Abstract/ZDomain.v @@ -8,7 +8,7 @@ (* Evgeny Makarov, INRIA, 2007 *) (************************************************************************) -(*i i*) +(*i $Id$ i*) Require Export NumPrelude. diff --git a/theories/Numbers/Integer/Abstract/ZLt.v b/theories/Numbers/Integer/Abstract/ZLt.v index 65a938e54..3d21444ad 100644 --- a/theories/Numbers/Integer/Abstract/ZLt.v +++ b/theories/Numbers/Integer/Abstract/ZLt.v @@ -8,7 +8,7 @@ (* Evgeny Makarov, INRIA, 2007 *) (************************************************************************) -(*i i*) +(*i $Id$ i*) Require Export ZTimes. diff --git a/theories/Numbers/Integer/Abstract/ZPlus.v b/theories/Numbers/Integer/Abstract/ZPlus.v index cbe22077e..cdafa1ca7 100644 --- a/theories/Numbers/Integer/Abstract/ZPlus.v +++ b/theories/Numbers/Integer/Abstract/ZPlus.v @@ -8,7 +8,7 @@ (* Evgeny Makarov, INRIA, 2007 *) (************************************************************************) -(*i i*) +(*i $Id$ i*) Require Export ZBase. diff --git a/theories/Numbers/Integer/Abstract/ZPlusOrder.v b/theories/Numbers/Integer/Abstract/ZPlusOrder.v index 079fc356d..3e6421819 100644 --- a/theories/Numbers/Integer/Abstract/ZPlusOrder.v +++ b/theories/Numbers/Integer/Abstract/ZPlusOrder.v @@ -8,7 +8,7 @@ (* Evgeny Makarov, INRIA, 2007 *) (************************************************************************) -(*i i*) +(*i $Id$ i*) Require Export ZLt. diff --git a/theories/Numbers/Integer/Abstract/ZTimes.v b/theories/Numbers/Integer/Abstract/ZTimes.v index 2ff8fd8da..7819dc085 100644 --- a/theories/Numbers/Integer/Abstract/ZTimes.v +++ b/theories/Numbers/Integer/Abstract/ZTimes.v @@ -8,7 +8,7 @@ (* Evgeny Makarov, INRIA, 2007 *) (************************************************************************) -(*i i*) +(*i $Id$ i*) Require Export ZPlus. diff --git a/theories/Numbers/Integer/Abstract/ZTimesOrder.v b/theories/Numbers/Integer/Abstract/ZTimesOrder.v index 0f4cb54a8..6b6f34d75 100644 --- a/theories/Numbers/Integer/Abstract/ZTimesOrder.v +++ b/theories/Numbers/Integer/Abstract/ZTimesOrder.v @@ -8,7 +8,7 @@ (* Evgeny Makarov, INRIA, 2007 *) (************************************************************************) -(*i i*) +(*i $Id$ i*) Require Export ZPlusOrder. diff --git a/theories/Numbers/Integer/BigZ/BigZ.v b/theories/Numbers/Integer/BigZ/BigZ.v index 8c7c1f809..934fbc428 100644 --- a/theories/Numbers/Integer/BigZ/BigZ.v +++ b/theories/Numbers/Integer/BigZ/BigZ.v @@ -1,3 +1,15 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) +(* Benjamin Gregoire, Laurent Thery, INRIA, 2007 *) +(************************************************************************) + +(*i $Id$ i*) + Require Export BigN. Require Import ZMake. diff --git a/theories/Numbers/Integer/BigZ/ZMake.v b/theories/Numbers/Integer/BigZ/ZMake.v index da65d276f..5927c2bea 100644 --- a/theories/Numbers/Integer/BigZ/ZMake.v +++ b/theories/Numbers/Integer/BigZ/ZMake.v @@ -5,6 +5,10 @@ (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +(* Benjamin Gregoire, Laurent Thery, INRIA, 2007 *) +(************************************************************************) + +(*i $Id$ i*) Require Import ZArith. Require Import BigNumPrelude. diff --git a/theories/Numbers/Integer/NatPairs/ZNatPairs.v b/theories/Numbers/Integer/NatPairs/ZNatPairs.v index a40832507..3f5583927 100644 --- a/theories/Numbers/Integer/NatPairs/ZNatPairs.v +++ b/theories/Numbers/Integer/NatPairs/ZNatPairs.v @@ -8,7 +8,7 @@ (* Evgeny Makarov, INRIA, 2007 *) (************************************************************************) -(*i i*) +(*i $Id$ i*) Require Import NMinus. (* The most complete file for natural numbers *) Require Export ZTimesOrder. (* The most complete file for integers *) diff --git a/theories/Numbers/NatInt/NZAxioms.v b/theories/Numbers/NatInt/NZAxioms.v index 6bdfe5642..0d3b251f3 100644 --- a/theories/Numbers/NatInt/NZAxioms.v +++ b/theories/Numbers/NatInt/NZAxioms.v @@ -8,7 +8,7 @@ (* Evgeny Makarov, INRIA, 2007 *) (************************************************************************) -(*i i*) +(*i $Id$ i*) Require Export NumPrelude. diff --git a/theories/Numbers/NatInt/NZBase.v b/theories/Numbers/NatInt/NZBase.v index 2e5b585bb..0b917e998 100644 --- a/theories/Numbers/NatInt/NZBase.v +++ b/theories/Numbers/NatInt/NZBase.v @@ -8,7 +8,7 @@ (* Evgeny Makarov, INRIA, 2007 *) (************************************************************************) -(*i i*) +(*i $Id$ i*) Require Import NZAxioms. diff --git a/theories/Numbers/NatInt/NZOrder.v b/theories/Numbers/NatInt/NZOrder.v index 133bbde4d..b11b84092 100644 --- a/theories/Numbers/NatInt/NZOrder.v +++ b/theories/Numbers/NatInt/NZOrder.v @@ -8,7 +8,7 @@ (* Evgeny Makarov, INRIA, 2007 *) (************************************************************************) -(*i i*) +(*i $Id$ i*) Require Import NZAxioms. Require Import NZTimes. diff --git a/theories/Numbers/NatInt/NZPlus.v b/theories/Numbers/NatInt/NZPlus.v index 7a4c7719b..673b819ba 100644 --- a/theories/Numbers/NatInt/NZPlus.v +++ b/theories/Numbers/NatInt/NZPlus.v @@ -8,7 +8,7 @@ (* Evgeny Makarov, INRIA, 2007 *) (************************************************************************) -(*i i*) +(*i $Id$ i*) Require Import NZAxioms. Require Import NZBase. diff --git a/theories/Numbers/NatInt/NZPlusOrder.v b/theories/Numbers/NatInt/NZPlusOrder.v index 9f1ba0f84..45148bc20 100644 --- a/theories/Numbers/NatInt/NZPlusOrder.v +++ b/theories/Numbers/NatInt/NZPlusOrder.v @@ -8,7 +8,7 @@ (* Evgeny Makarov, INRIA, 2007 *) (************************************************************************) -(*i i*) +(*i $Id$ i*) Require Import NZAxioms. Require Import NZOrder. diff --git a/theories/Numbers/NatInt/NZTimes.v b/theories/Numbers/NatInt/NZTimes.v index 20bd3cdc6..7503ddce2 100644 --- a/theories/Numbers/NatInt/NZTimes.v +++ b/theories/Numbers/NatInt/NZTimes.v @@ -8,7 +8,7 @@ (* Evgeny Makarov, INRIA, 2007 *) (************************************************************************) -(*i i*) +(*i $Id$ i*) Require Import NZAxioms. Require Import NZPlus. diff --git a/theories/Numbers/NatInt/NZTimesOrder.v b/theories/Numbers/NatInt/NZTimesOrder.v index b51e3d22b..b48acc598 100644 --- a/theories/Numbers/NatInt/NZTimesOrder.v +++ b/theories/Numbers/NatInt/NZTimesOrder.v @@ -8,7 +8,7 @@ (* Evgeny Makarov, INRIA, 2007 *) (************************************************************************) -(*i i*) +(*i $Id$ i*) Require Import NZAxioms. Require Import NZPlusOrder. diff --git a/theories/Numbers/Natural/Abstract/NAxioms.v b/theories/Numbers/Natural/Abstract/NAxioms.v index 86a828d03..8bd57b988 100644 --- a/theories/Numbers/Natural/Abstract/NAxioms.v +++ b/theories/Numbers/Natural/Abstract/NAxioms.v @@ -8,7 +8,7 @@ (* Evgeny Makarov, INRIA, 2007 *) (************************************************************************) -(*i i*) +(*i $Id$ i*) Require Export NZAxioms. diff --git a/theories/Numbers/Natural/Abstract/NBase.v b/theories/Numbers/Natural/Abstract/NBase.v index 1a11f7a13..e90977e3d 100644 --- a/theories/Numbers/Natural/Abstract/NBase.v +++ b/theories/Numbers/Natural/Abstract/NBase.v @@ -8,7 +8,7 @@ (* Evgeny Makarov, INRIA, 2007 *) (************************************************************************) -(*i i*) +(*i $Id$ i*) Require Export Decidable. Require Export NAxioms. diff --git a/theories/Numbers/Natural/Abstract/NDefOps.v b/theories/Numbers/Natural/Abstract/NDefOps.v index 027bfd3ce..369c1261c 100644 --- a/theories/Numbers/Natural/Abstract/NDefOps.v +++ b/theories/Numbers/Natural/Abstract/NDefOps.v @@ -1,3 +1,15 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) +(* Evgeny Makarov, INRIA, 2007 *) +(************************************************************************) + +(*i $Id$ i*) + Require Import Bool. (* To get the orb and negb function *) Require Export NStrongRec. diff --git a/theories/Numbers/Natural/Abstract/NIso.v b/theories/Numbers/Natural/Abstract/NIso.v index 4df46e20e..5ad343fe0 100644 --- a/theories/Numbers/Natural/Abstract/NIso.v +++ b/theories/Numbers/Natural/Abstract/NIso.v @@ -8,7 +8,7 @@ (* Evgeny Makarov, INRIA, 2007 *) (************************************************************************) -(*i i*) +(*i $Id$ i*) Require Import NBase. diff --git a/theories/Numbers/Natural/Abstract/NMinus.v b/theories/Numbers/Natural/Abstract/NMinus.v index 5e1d5d8c3..0c24ca984 100644 --- a/theories/Numbers/Natural/Abstract/NMinus.v +++ b/theories/Numbers/Natural/Abstract/NMinus.v @@ -8,7 +8,7 @@ (* Evgeny Makarov, INRIA, 2007 *) (************************************************************************) -(*i i*) +(*i $Id$ i*) Require Export NTimesOrder. diff --git a/theories/Numbers/Natural/Abstract/NOrder.v b/theories/Numbers/Natural/Abstract/NOrder.v index 1e53d8063..bc5753d16 100644 --- a/theories/Numbers/Natural/Abstract/NOrder.v +++ b/theories/Numbers/Natural/Abstract/NOrder.v @@ -8,7 +8,7 @@ (* Evgeny Makarov, INRIA, 2007 *) (************************************************************************) -(*i i*) +(*i $Id$ i*) Require Export NTimes. diff --git a/theories/Numbers/Natural/Abstract/NPlus.v b/theories/Numbers/Natural/Abstract/NPlus.v index 09b5a500b..71122e3a5 100644 --- a/theories/Numbers/Natural/Abstract/NPlus.v +++ b/theories/Numbers/Natural/Abstract/NPlus.v @@ -8,7 +8,7 @@ (* Evgeny Makarov, INRIA, 2007 *) (************************************************************************) -(*i i*) +(*i $Id$ i*) Require Export NBase. diff --git a/theories/Numbers/Natural/Abstract/NPlusOrder.v b/theories/Numbers/Natural/Abstract/NPlusOrder.v index 265ea8144..8a8addefc 100644 --- a/theories/Numbers/Natural/Abstract/NPlusOrder.v +++ b/theories/Numbers/Natural/Abstract/NPlusOrder.v @@ -8,7 +8,7 @@ (* Evgeny Makarov, INRIA, 2007 *) (************************************************************************) -(*i i*) +(*i $Id$ i*) Require Export NOrder. diff --git a/theories/Numbers/Natural/Abstract/NStrongRec.v b/theories/Numbers/Natural/Abstract/NStrongRec.v index ace608dbe..78b647d99 100644 --- a/theories/Numbers/Natural/Abstract/NStrongRec.v +++ b/theories/Numbers/Natural/Abstract/NStrongRec.v @@ -8,7 +8,7 @@ (* Evgeny Makarov, INRIA, 2007 *) (************************************************************************) -(*i i*) +(*i $Id$ i*) (** This file defined the strong (course-of-value, well-founded) recursion and proves its properties *) diff --git a/theories/Numbers/Natural/Abstract/NTimes.v b/theories/Numbers/Natural/Abstract/NTimes.v index 7d513dc46..8c0132dd9 100644 --- a/theories/Numbers/Natural/Abstract/NTimes.v +++ b/theories/Numbers/Natural/Abstract/NTimes.v @@ -8,7 +8,7 @@ (* Evgeny Makarov, INRIA, 2007 *) (************************************************************************) -(*i i*) +(*i $Id$ i*) Require Export NPlus. diff --git a/theories/Numbers/Natural/Abstract/NTimesOrder.v b/theories/Numbers/Natural/Abstract/NTimesOrder.v index 259416d46..15d99c757 100644 --- a/theories/Numbers/Natural/Abstract/NTimesOrder.v +++ b/theories/Numbers/Natural/Abstract/NTimesOrder.v @@ -8,7 +8,7 @@ (* Evgeny Makarov, INRIA, 2007 *) (************************************************************************) -(*i i*) +(*i $Id$ i*) Require Export NPlusOrder. diff --git a/theories/Numbers/Natural/BigN/BigN.v b/theories/Numbers/Natural/BigN/BigN.v index b64a853fd..ecb4578eb 100644 --- a/theories/Numbers/Natural/BigN/BigN.v +++ b/theories/Numbers/Natural/BigN/BigN.v @@ -6,6 +6,8 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +(*i $Id$ i*) + (** * Natural numbers in base 2^31 *) (** diff --git a/theories/Numbers/Natural/BigN/NMake_gen.ml b/theories/Numbers/Natural/BigN/NMake_gen.ml index 347485eeb..a180ed1e0 100644 --- a/theories/Numbers/Natural/BigN/NMake_gen.ml +++ b/theories/Numbers/Natural/BigN/NMake_gen.ml @@ -5,6 +5,8 @@ (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +(* Benjamin Gregoire, Laurent Thery, INRIA, 2007 *) +(************************************************************************) (*i $Id$ i*) @@ -58,15 +60,14 @@ let _ = pr "(* // * This file is distributed under the terms of the *)"; pr "(* * GNU Lesser General Public License Version 2.1 *)"; pr "(************************************************************************)"; + pr "(* Benjamin Gregoire, Laurent Thery, INRIA, 2007 *)"; + pr "(************************************************************************)"; pr ""; pr "(** * NMake *)"; pr ""; - pr "(** From a cyclic Z/nZ representation to arbitrary precision natural numbers."; - pr "- Authors: Benjamin Grégoire, Laurent Théry"; - pr "- Institution: INRIA"; - pr "- Date: 2007"; - pr "- Remark: File automatically generated by NMake_gen.ml, DO NOT EDIT !"; - pr "*)"; + pr "(** From a cyclic Z/nZ representation to arbitrary precision natural numbers.*)"; + pr ""; + pr "(** Remark: File automatically generated by NMake_gen.ml, DO NOT EDIT ! *)"; pr ""; pr "Require Import BigNumPrelude."; pr "Require Import ZArith."; diff --git a/theories/Numbers/Natural/BigN/Nbasic.v b/theories/Numbers/Natural/BigN/Nbasic.v index 3d20c35ce..9ca078053 100644 --- a/theories/Numbers/Natural/BigN/Nbasic.v +++ b/theories/Numbers/Natural/BigN/Nbasic.v @@ -5,6 +5,10 @@ (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +(* Benjamin Gregoire, Laurent Thery, INRIA, 2007 *) +(************************************************************************) + +(*i $Id$ i*) Require Import ZArith. Require Import BigNumPrelude. diff --git a/theories/Numbers/Natural/Binary/NBinDefs.v b/theories/Numbers/Natural/Binary/NBinDefs.v index 3110da36a..c2af66724 100644 --- a/theories/Numbers/Natural/Binary/NBinDefs.v +++ b/theories/Numbers/Natural/Binary/NBinDefs.v @@ -8,7 +8,7 @@ (* Evgeny Makarov, INRIA, 2007 *) (************************************************************************) -(*i i*) +(*i $Id$ i*) Require Import BinPos. Require Export BinNat. diff --git a/theories/Numbers/Natural/Binary/NBinary.v b/theories/Numbers/Natural/Binary/NBinary.v index bf4432c38..558f2d0e4 100644 --- a/theories/Numbers/Natural/Binary/NBinary.v +++ b/theories/Numbers/Natural/Binary/NBinary.v @@ -1,3 +1,15 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) +(* Evgeny Makarov, INRIA, 2007 *) +(************************************************************************) + +(*i $Id$ i*) + Require Export NBinDefs. Require Export NArithRing. diff --git a/theories/Numbers/Natural/Peano/NPeano.v b/theories/Numbers/Natural/Peano/NPeano.v index 26a6053eb..506cf1df0 100644 --- a/theories/Numbers/Natural/Peano/NPeano.v +++ b/theories/Numbers/Natural/Peano/NPeano.v @@ -8,7 +8,7 @@ (* Evgeny Makarov, INRIA, 2007 *) (************************************************************************) -(*i i*) +(*i $Id$ i*) Require Import Arith. Require Import Min. diff --git a/theories/Numbers/NumPrelude.v b/theories/Numbers/NumPrelude.v index f042ab068..2c221a88e 100644 --- a/theories/Numbers/NumPrelude.v +++ b/theories/Numbers/NumPrelude.v @@ -8,7 +8,7 @@ (* Evgeny Makarov, INRIA, 2007 *) (************************************************************************) -(*i i*) +(*i $Id$ i*) Require Export Setoid. (*Require Export Bool.*) diff --git a/theories/Numbers/QRewrite.v b/theories/Numbers/QRewrite.v index 4fc7ce197..49e0b3e78 100644 --- a/theories/Numbers/QRewrite.v +++ b/theories/Numbers/QRewrite.v @@ -8,7 +8,7 @@ (* Evgeny Makarov, INRIA, 2007 *) (************************************************************************) -(*i i*) +(*i $Id$ i*) Require Import List. Require Import Setoid. diff --git a/theories/Numbers/Rational/BigQ/BigQ.v b/theories/Numbers/Rational/BigQ/BigQ.v index 33e5f669c..c7c7735c0 100644 --- a/theories/Numbers/Rational/BigQ/BigQ.v +++ b/theories/Numbers/Rational/BigQ/BigQ.v @@ -5,8 +5,10 @@ (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +(* Benjamin Gregoire, Laurent Thery, INRIA, 2007 *) +(************************************************************************) -(* *) +(*i $Id$ i*) Require Export QMake_base. Require Import QpMake. diff --git a/theories/Numbers/Rational/BigQ/Q0Make.v b/theories/Numbers/Rational/BigQ/Q0Make.v index e075bdb15..4260c954f 100644 --- a/theories/Numbers/Rational/BigQ/Q0Make.v +++ b/theories/Numbers/Rational/BigQ/Q0Make.v @@ -5,6 +5,10 @@ (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +(* Benjamin Gregoire, Laurent Thery, INRIA, 2007 *) +(************************************************************************) + +(*i $Id$ i*) Require Import Bool. Require Import ZArith. diff --git a/theories/Numbers/Rational/BigQ/QMake_base.v b/theories/Numbers/Rational/BigQ/QMake_base.v index e12c78581..6c54ed5ad 100644 --- a/theories/Numbers/Rational/BigQ/QMake_base.v +++ b/theories/Numbers/Rational/BigQ/QMake_base.v @@ -5,17 +5,13 @@ (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +(* Benjamin Gregoire, Laurent Thery, INRIA, 2007 *) +(************************************************************************) (* $Id$ *) (** * An implementation of rational numbers based on big integers *) -(** -- Authors: Benjamin Grégoire, Laurent Théry -- Institution: INRIA -- Date: 2007 -*) - Require Export BigN. Require Export BigZ. diff --git a/theories/Numbers/Rational/BigQ/QbiMake.v b/theories/Numbers/Rational/BigQ/QbiMake.v index 8420a5360..8ce671a73 100644 --- a/theories/Numbers/Rational/BigQ/QbiMake.v +++ b/theories/Numbers/Rational/BigQ/QbiMake.v @@ -5,6 +5,10 @@ (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +(* Benjamin Gregoire, Laurent Thery, INRIA, 2007 *) +(************************************************************************) + +(*i $Id$ i*) Require Import Bool. Require Import ZArith. diff --git a/theories/Numbers/Rational/BigQ/QifMake.v b/theories/Numbers/Rational/BigQ/QifMake.v index 6df06bdf2..436c13758 100644 --- a/theories/Numbers/Rational/BigQ/QifMake.v +++ b/theories/Numbers/Rational/BigQ/QifMake.v @@ -5,6 +5,10 @@ (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +(* Benjamin Gregoire, Laurent Thery, INRIA, 2007 *) +(************************************************************************) + +(*i $Id$ i*) Require Import Bool. Require Import ZArith. diff --git a/theories/Numbers/Rational/BigQ/QpMake.v b/theories/Numbers/Rational/BigQ/QpMake.v index a194431ec..db6c5926f 100644 --- a/theories/Numbers/Rational/BigQ/QpMake.v +++ b/theories/Numbers/Rational/BigQ/QpMake.v @@ -5,6 +5,10 @@ (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +(* Benjamin Gregoire, Laurent Thery, INRIA, 2007 *) +(************************************************************************) + +(*i $Id$ i*) Require Import Bool. Require Import ZArith. diff --git a/theories/Numbers/Rational/BigQ/QvMake.v b/theories/Numbers/Rational/BigQ/QvMake.v index 1282c8694..59da4da6d 100644 --- a/theories/Numbers/Rational/BigQ/QvMake.v +++ b/theories/Numbers/Rational/BigQ/QvMake.v @@ -5,6 +5,10 @@ (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +(* Benjamin Gregoire, Laurent Thery, INRIA, 2007 *) +(************************************************************************) + +(*i $Id$ i*) Require Import Bool. Require Import ZArith. |