diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-05-22 11:08:13 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-05-22 11:08:13 +0000 |
| commit | cf73432c0e850242c7918cc348388e5cde379a8f (patch) | |
| tree | 07ebc5fa4588f13416caaca476f90816beb867ae /theories/Numbers/Cyclic/DoubleCyclic/DoubleAdd.v | |
| parent | 313de91c9cd26e6fee94aa5bb093ae8a436fd43a (diff) | |
switch theories/Numbers from Set to Type (both the abstract and the bignum part).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10964 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Numbers/Cyclic/DoubleCyclic/DoubleAdd.v')
| -rw-r--r-- | theories/Numbers/Cyclic/DoubleCyclic/DoubleAdd.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/theories/Numbers/Cyclic/DoubleCyclic/DoubleAdd.v b/theories/Numbers/Cyclic/DoubleCyclic/DoubleAdd.v index d198361f1..d60af33ec 100644 --- a/theories/Numbers/Cyclic/DoubleCyclic/DoubleAdd.v +++ b/theories/Numbers/Cyclic/DoubleCyclic/DoubleAdd.v @@ -20,7 +20,7 @@ Require Import DoubleBase. Open Local Scope Z_scope. Section DoubleAdd. - Variable w : Set. + Variable w : Type. Variable w_0 : w. Variable w_1 : w. Variable w_WW : w -> w -> zn2z w. @@ -76,7 +76,7 @@ Section DoubleAdd. end end. - Variable R : Set. + Variable R : Type. Variable f0 f1 : zn2z w -> R. Definition ww_add_c_cont x y := |