aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Numbers/Cyclic/Abstract/ZnZ.v
diff options
context:
space:
mode:
Diffstat (limited to 'theories/Numbers/Cyclic/Abstract/ZnZ.v')
-rw-r--r--theories/Numbers/Cyclic/Abstract/ZnZ.v8
1 files changed, 1 insertions, 7 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.