diff options
57 files changed, 210 insertions, 130 deletions
diff --git a/theories/Numbers/BigNumPrelude.v b/theories/Numbers/BigNumPrelude.v index 8e4b1d64f0..586e501679 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 dfe0912092..877e49c11e 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 2116aaddd3..60fa09584f 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 889ccaa4d5..68703129b1 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 2283e3ca0c..eb517c0607 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 0e9993b10e..057ad3c065 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 a686f0c275..cbf487f4b4 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 5f8b00a52f..6cc1ecad3f 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 57cdeeb884..f42946d6f1 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 f8cb16858b..ce312aa62a 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 b96d09562c..3babd77166 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 9b77cf0390..a70f3c8ecd 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 d7e80d4a28..032326c81f 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 fdc7bab4cb..678781b23c 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 0813a3caae..c57f9ede0c 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 51b522a52d..ce3ca21c2b 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 65a938e54d..3d21444ad0 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 cbe22077e0..cdafa1ca7c 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 079fc356d8..3e6421819b 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 2ff8fd8dae..7819dc085f 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 0f4cb54a8a..6b6f34d75e 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 8c7c1f809c..934fbc4280 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 da65d276fb..5927c2beab 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 a40832507d..3f5583927a 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 6bdfe56426..0d3b251f39 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 2e5b585bb3..0b917e9983 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 133bbde4df..b11b840928 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 7a4c7719bf..673b819ba4 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 9f1ba0f84b..45148bc20c 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 20bd3cdc61..7503ddce22 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 b51e3d22b6..b48acc598d 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 86a828d037..8bd57b9888 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 1a11f7a131..e90977e3d7 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 027bfd3ce6..369c1261cf 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 4df46e20eb..5ad343fe09 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 5e1d5d8c3c..0c24ca9849 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 1e53d80637..bc5753d167 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 09b5a500b3..71122e3a5a 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 265ea81444..8a8addefc7 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 ace608dbe0..78b647d995 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 7d513dc460..8c0132dd99 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 259416d468..15d99c7575 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 b64a853fd6..ecb4578ebe 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 347485eeb8..a180ed1e03 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 3d20c35cec..9ca078053d 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 3110da36a6..c2af667247 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 bf4432c38a..558f2d0e49 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 26a6053eb1..506cf1df07 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 f042ab0685..2c221a88e7 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 4fc7ce197d..49e0b3e787 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 33e5f669cd..c7c7735c0a 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 e075bdb150..4260c954f3 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 e12c785813..6c54ed5ad3 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 8420a53600..8ce671a73e 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 6df06bdf22..436c137585 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 a194431ec4..db6c5926fe 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 1282c86948..59da4da6df 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. |