From a3ff3200aa6a9235f314575a16f8052a94896b2b Mon Sep 17 00:00:00 2001 From: aspiwack Date: Wed, 18 Jul 2007 14:57:10 +0000 Subject: J'ai enlevé un fichier qui était en double. Merci à Pierre pour avoir noté cette erreur de ma part (copier/coller mon amour). Ça créait des soucis dans les dépendance dans l'ancienne architecture de Makefile, probablement dans la nouvelle aussi dans certaines circonstances. Exit les bêtise, c'est plus propre maintenant. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10019 85f007b7-540e-0410-9357-904b9bb8a0f7 --- theories/Ints/num/Basic_type.v | 64 ------------------------------------------ 1 file changed, 64 deletions(-) delete mode 100644 theories/Ints/num/Basic_type.v diff --git a/theories/Ints/num/Basic_type.v b/theories/Ints/num/Basic_type.v deleted file mode 100644 index f481f39427..0000000000 --- a/theories/Ints/num/Basic_type.v +++ /dev/null @@ -1,64 +0,0 @@ - -(*************************************************************) -(* 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 *) -(*************************************************************) - -Set Implicit Arguments. - -Require Import ZArith. -Require Import ZDivModAux. -Require Import ZPowerAux. - -Open Local Scope Z_scope. - -Section Carry. - - Variable A : Set. - - Inductive carry : Set := - | C0 : A -> carry - | C1 : A -> carry. - -End Carry. - -Section Zn2Z. - - Variable znz : Set. - - Inductive zn2z : Set := - | W0 : zn2z - | WW : znz -> znz -> zn2z. - - Definition zn2z_to_Z (wB:Z) (w_to_Z:znz->Z) (x:zn2z) := - match x with - | W0 => 0 - | WW xh xl => w_to_Z xh * wB + w_to_Z xl - end. - - Definition base digits := Zpower 2 (Zpos digits). - - Definition interp_carry sign B (interp:znz -> Z) c := - match c with - | C0 x => interp x - | C1 x => sign*B + interp x - end. - -End Zn2Z. - -Implicit Arguments W0 [znz]. - -Fixpoint word_tr (w:Set) (n:nat) {struct n} : Set := - match n with - | O => w - | S n => word_tr (zn2z w) n - end. - -Fixpoint word (w:Set) (n:nat) {struct n} : Set := - match n with - | O => w - | S n => zn2z (word w n) - end. - -- cgit v1.2.3