From 0b4c7d793500e63aa11ae31ee53ada5758709dea Mon Sep 17 00:00:00 2001
From: bertot
Date: Fri, 7 Jun 2002 09:44:51 +0000
Subject: Adding file theories/ZArith/Zsqrt.v that contains a square root
 function. actually three functions are provided, one working on positive
 numbers (it is structurally recursive), one with a strong specification
 (Zsqrt), and one with a weak specification (Zsqrt_plain).  For the function
 with a weak specification an extra theorem is also provided.

The decision functions in ZArith_dec have been made transparent so that computation
with the square root function also becomes possible with Lazy Beta Iota Delta Zeta.


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2770 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 Makefile | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'Makefile')

diff --git a/Makefile b/Makefile
index b5ff0809bf..4f6463060d 100644
--- a/Makefile
+++ b/Makefile
@@ -454,7 +454,7 @@ ZARITHVO=theories/ZArith/Wf_Z.vo        theories/ZArith/Zsyntax.vo \
 	 theories/ZArith/Zmisc.vo       theories/ZArith/zarith_aux.vo \
 	 theories/ZArith/Zhints.vo	theories/ZArith/Zlogarithm.vo \
 	 theories/ZArith/Zpower.vo 	theories/ZArith/Zcomplements.vo \
-	 theories/ZArith/Zdiv.vo
+	 theories/ZArith/Zdiv.vo	theories/ZArith/Zsqrt.vo
 
 LISTSVO=theories/Lists/List.vo      theories/Lists/PolyListSyntax.vo \
         theories/Lists/ListSet.vo   theories/Lists/Streams.vo \
-- 
cgit v1.2.3