From d9acd0a5dc55d422e18e8caf318dc325c16c2535 Mon Sep 17 00:00:00 2001
From: letouzey
Date: Thu, 20 Sep 2001 14:14:35 +0000
Subject: changements mineurs du test

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2020 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 contrib/extraction/test/.depend     | 22 ++++++++++++----------
 contrib/extraction/test/Makefile    |  6 ++++--
 contrib/extraction/test/addReals    | 25 +++++++++++++++++++++++++
 contrib/extraction/test/addReals.ml | 25 -------------------------
 4 files changed, 41 insertions(+), 37 deletions(-)
 create mode 100644 contrib/extraction/test/addReals
 delete mode 100644 contrib/extraction/test/addReals.ml

diff --git a/contrib/extraction/test/.depend b/contrib/extraction/test/.depend
index a01546554f..89ca9205c2 100644
--- a/contrib/extraction/test/.depend
+++ b/contrib/extraction/test/.depend
@@ -160,20 +160,22 @@ theories/Reals/addReals.cmo: theories/ZArith/fast_integer.cmo \
     theories/Reals/typeSyntax.cmo 
 theories/Reals/addReals.cmx: theories/ZArith/fast_integer.cmx \
     theories/Reals/typeSyntax.cmx 
-theories/Reals/r_Ifp.cmo: addReals.cmo theories/ZArith/fast_integer.cmo \
-    theories/Reals/raxioms.cmo theories/Reals/rdefinitions.cmo \
-    theories/ZArith/zarith_aux.cmo 
-theories/Reals/r_Ifp.cmx: addReals.cmx theories/ZArith/fast_integer.cmx \
-    theories/Reals/raxioms.cmx theories/Reals/rdefinitions.cmx \
-    theories/ZArith/zarith_aux.cmx 
+theories/Reals/r_Ifp.cmo: theories/Reals/addReals.cmo \
+    theories/ZArith/fast_integer.cmo theories/Reals/raxioms.cmo \
+    theories/Reals/rdefinitions.cmo theories/ZArith/zarith_aux.cmo 
+theories/Reals/r_Ifp.cmx: theories/Reals/addReals.cmx \
+    theories/ZArith/fast_integer.cmx theories/Reals/raxioms.cmx \
+    theories/Reals/rdefinitions.cmx theories/ZArith/zarith_aux.cmx 
 theories/Reals/raxioms.cmo: theories/Init/datatypes.cmo \
     theories/ZArith/fast_integer.cmo 
 theories/Reals/raxioms.cmx: theories/Init/datatypes.cmx \
     theories/ZArith/fast_integer.cmx 
-theories/Reals/rbase.cmo: addReals.cmo theories/Init/specif.cmo \
-    theories/Reals/typeSyntax.cmo theories/ZArith/zarith_aux.cmo 
-theories/Reals/rbase.cmx: addReals.cmx theories/Init/specif.cmx \
-    theories/Reals/typeSyntax.cmx theories/ZArith/zarith_aux.cmx 
+theories/Reals/rbase.cmo: theories/Reals/addReals.cmo \
+    theories/Init/specif.cmo theories/Reals/typeSyntax.cmo \
+    theories/ZArith/zarith_aux.cmo 
+theories/Reals/rbase.cmx: theories/Reals/addReals.cmx \
+    theories/Init/specif.cmx theories/Reals/typeSyntax.cmx \
+    theories/ZArith/zarith_aux.cmx 
 theories/Reals/rbasic_fun.cmo: theories/Reals/rbase.cmo \
     theories/Reals/typeSyntax.cmo 
 theories/Reals/rbasic_fun.cmx: theories/Reals/rbase.cmx \
diff --git a/contrib/extraction/test/Makefile b/contrib/extraction/test/Makefile
index fd37b46872..e3e44e0513 100644
--- a/contrib/extraction/test/Makefile
+++ b/contrib/extraction/test/Makefile
@@ -31,7 +31,7 @@ CMO:= $(patsubst %.ml,%.cmo,$(ML))
 #	General rules 
 #
 
-all: $(ML) depend $(CMO) v2ml
+all: $(ML) $(CMO) v2ml
 
 depend: $(ML)
 	rm -f .depend; ocamldep $(INCL) theories/*/*.ml > .depend
@@ -62,7 +62,9 @@ reals: all $(REALSML) theories/Reals/addReals.cmo $(REALSCMO)
 
 realsml: 
 	./extract_reals $(REALSVO)
-	cp -f addReals.ml theories/Reals
+
+theories/Reals/addReals.ml: 
+	cp -f addReals theories/Reals/addReals.ml
 
 $(REALSML): realsml
 
diff --git a/contrib/extraction/test/addReals b/contrib/extraction/test/addReals
new file mode 100644
index 0000000000..86e9a79947
--- /dev/null
+++ b/contrib/extraction/test/addReals
@@ -0,0 +1,25 @@
+let total_order_T x y = 
+if x = y then
+        TypeSyntax.Coq_inleftT TypeSyntax.Coq_rightT
+else if x < y then
+        TypeSyntax.Coq_inleftT TypeSyntax.Coq_leftT
+else    TypeSyntax.Coq_inrightT 
+
+let rec int_to_positive i = 
+	if i = 1 then 
+	  Fast_integer.Coq_xH
+	else
+	  if (i mod 2) = 0 then 
+	      Fast_integer.Coq_xO (int_to_positive (i/2))
+	  else 
+	      Fast_integer.Coq_xI (int_to_positive (i/2))
+
+let rec int_to_Z i = 
+	if i = 0 then 
+	  Fast_integer.ZERO
+	else if i > 0 then 
+	  Fast_integer.POS (int_to_positive i)
+	else 
+	  Fast_integer.NEG (int_to_positive (-i))
+
+let my_ceil x = int_to_Z (int_of_float (ceil x))
diff --git a/contrib/extraction/test/addReals.ml b/contrib/extraction/test/addReals.ml
deleted file mode 100644
index 86e9a79947..0000000000
--- a/contrib/extraction/test/addReals.ml
+++ /dev/null
@@ -1,25 +0,0 @@
-let total_order_T x y = 
-if x = y then
-        TypeSyntax.Coq_inleftT TypeSyntax.Coq_rightT
-else if x < y then
-        TypeSyntax.Coq_inleftT TypeSyntax.Coq_leftT
-else    TypeSyntax.Coq_inrightT 
-
-let rec int_to_positive i = 
-	if i = 1 then 
-	  Fast_integer.Coq_xH
-	else
-	  if (i mod 2) = 0 then 
-	      Fast_integer.Coq_xO (int_to_positive (i/2))
-	  else 
-	      Fast_integer.Coq_xI (int_to_positive (i/2))
-
-let rec int_to_Z i = 
-	if i = 0 then 
-	  Fast_integer.ZERO
-	else if i > 0 then 
-	  Fast_integer.POS (int_to_positive i)
-	else 
-	  Fast_integer.NEG (int_to_positive (-i))
-
-let my_ceil x = int_to_Z (int_of_float (ceil x))
-- 
cgit v1.2.3