diff options
author | 2003-11-05 13:43:45 +0000 | |
---|---|---|
committer | 2003-11-05 13:43:45 +0000 | |
commit | b1e1be15990aef3fd76b28fad3d52cf6bc36a60b (patch) | |
tree | d9d4944e0cd7267e99583405a63b6f72c53f6182 /theories/ZArith/Zsqrt.v | |
parent | 380a8c4a8e7fb56fa105a76694f60f262d27d1a1 (diff) |
Restructuration ZArith et déport de la partie sur 'positive' dans NArith, de la partie Omega dans contrib/omega
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4801 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/ZArith/Zsqrt.v')
-rw-r--r-- | theories/ZArith/Zsqrt.v | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/theories/ZArith/Zsqrt.v b/theories/ZArith/Zsqrt.v index 3c895d6db..e5ee2682d 100644 --- a/theories/ZArith/Zsqrt.v +++ b/theories/ZArith/Zsqrt.v @@ -14,6 +14,9 @@ Require Export Omega. V7only [Import Z_scope.]. Open Local Scope Z_scope. +(**********************************************************************) +(** Definition and properties of square root on Z *) + (** The following tactic replaces all instances of (POS (xI ...)) by `2*(POS ...)+1` , but only when ... is not made only with xO, XI, or xH. *) Tactic Definition compute_POS := |