Integration of theories/Ints into theories/Numbers, part 1: moving files

For the moment, the Ints files are simply moved into directories in
theories/Numbers with meaningful names. No filenames changed, apart
from: 
 Zaux.v -> theories/Numbers/BigNumPrelude.v 
 MemoFn.v -> theories/Lists/StreamMemo.v

More to come...



git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10899 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 0 insertions, 38 deletions

diff --git a/theories/Ints/num/QMake_base.v b/theories/Ints/num/QMake_base.v
deleted file mode 100644
index 0cd2d2122f..0000000000
--- a/theories/Ints/num/QMake_base.v
+++ /dev/null
@@ -1,38 +0,0 @@
-(************************************************************************)
-(*  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        *)
-(************************************************************************)
-
-(* $Id:$ *)
-
-(** * An implementation of rational numbers based on big integers *)
-
-(** 
-- Authors: Benjamin Grégoire, Laurent Théry
-- Institution: INRIA
-- Date: 2007
-*)
-
-Require Export BigN.
-Require Export BigZ.
-
-(* Basic type for Q: a Z or a pair of a Z and an N *)
-
-Inductive q_type : Set := 
- | Qz : BigZ.t -> q_type
- | Qq : BigZ.t -> BigN.t -> q_type.
-
-Definition print_type x := 
- match x with
- | Qz _ => Z
- | _ => (Z*Z)%type
- end.
-
-Definition print x :=
- match x return print_type x with
- | Qz zx => BigZ.to_Z zx
- | Qq nx dx => (BigZ.to_Z nx, BigN.to_Z dx)
- end.