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). MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Ç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 f481f3942..000000000 --- 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