From dccdf646ba050538c026706664b57229f38555c2 Mon Sep 17 00:00:00 2001 From: aspiwack Date: Sat, 2 Nov 2013 15:40:34 +0000 Subject: Restore Zsqrt compat now that refine works fine with match. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17021 85f007b7-540e-0410-9357-904b9bb8a0f7 --- theories/ZArith/Zsqrt_compat.v | 7 +------ 1 file changed, 1 insertion(+), 6 deletions(-) (limited to 'theories/ZArith') diff --git a/theories/ZArith/Zsqrt_compat.v b/theories/ZArith/Zsqrt_compat.v index bcfc4c7ac..9e8d9372c 100644 --- a/theories/ZArith/Zsqrt_compat.v +++ b/theories/ZArith/Zsqrt_compat.v @@ -96,9 +96,7 @@ Definition sqrtrempos : forall p:positive, sqrt_data (Zpos p). end end); clear sqrtrempos; repeat compute_POS; try (try rewrite Heq; ring); try omega. -(*arnaud: Admitted temporaire en attendant les modifs idoines de la compilation du pattern-matching -Defined.*) -Admitted. +Defined. (** Define with integer input, but with a strong (readable) specification. *) Definition Zsqrt : @@ -143,11 +141,8 @@ Definition Zsqrt : (fun r:Z => 0 = 0 * 0 + r /\ 0 * 0 <= 0 < (0 + 1) * (0 + 1)) 0 _) end); try omega. -(*arnaud: Admitted temporaire en attendant les modifs idoines de la compilation du pattern-matching split; [ omega | rewrite Heq; ring_simplify (s*s) ((s + 1) * (s + 1)); omega ]. Defined. -*) -Admitted. (** Define a function of type Z->Z that computes the integer square root, but only for positive numbers, and 0 for others. *) -- cgit v1.2.3