diff options
Diffstat (limited to 'theories/Numbers/Cyclic')
| -rw-r--r-- | theories/Numbers/Cyclic/Abstract/ZnZ.v | 8 | ||||
| -rw-r--r-- | theories/Numbers/Cyclic/DoubleCyclic/Basic_type.v | 9 | ||||
| -rw-r--r-- | theories/Numbers/Cyclic/DoubleCyclic/GenAdd.v | 9 | ||||
| -rw-r--r-- | theories/Numbers/Cyclic/DoubleCyclic/GenBase.v | 13 | ||||
| -rw-r--r-- | theories/Numbers/Cyclic/DoubleCyclic/GenDiv.v | 18 | ||||
| -rw-r--r-- | theories/Numbers/Cyclic/DoubleCyclic/GenDivn1.v | 18 | ||||
| -rw-r--r-- | theories/Numbers/Cyclic/DoubleCyclic/GenLift.v | 16 | ||||
| -rw-r--r-- | theories/Numbers/Cyclic/DoubleCyclic/GenMul.v | 18 | ||||
| -rw-r--r-- | theories/Numbers/Cyclic/DoubleCyclic/GenSqrt.v | 16 | ||||
| -rw-r--r-- | theories/Numbers/Cyclic/DoubleCyclic/GenSub.v | 18 | ||||
| -rw-r--r-- | theories/Numbers/Cyclic/DoubleCyclic/Zn2Z.v | 18 | ||||
| -rw-r--r-- | theories/Numbers/Cyclic/Int31/Int31.v | 4 |
12 files changed, 88 insertions, 77 deletions
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. |