diff options
| author |  aspiwack <aspiwack@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-07-18 14:57:10 +0000 |
|---|---|---|
| committer | aspiwack <aspiwack@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-07-18 14:57:10 +0000 |
| commit | a3ff3200aa6a9235f314575a16f8052a94896b2b (patch) | |
| tree | 27d517be1bb49f3141b91424a445d4404c24332a | |
| parent | 481bc97bfccd2ebd677da191a1e1e69fd4bbc70c (diff) | |
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
| -rw-r--r-- | theories/Ints/num/Basic_type.v | 64 |
1 files changed, 0 insertions, 64 deletions
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. - |