aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Numbers
diff options
context:
space:
mode:
Diffstat (limited to 'theories/Numbers')
-rw-r--r--theories/Numbers/Cyclic/DoubleCyclic/DoubleType.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/Numbers/Cyclic/DoubleCyclic/DoubleType.v b/theories/Numbers/Cyclic/DoubleCyclic/DoubleType.v
index ce1c0bef1..900cb1db5 100644
--- a/theories/Numbers/Cyclic/DoubleCyclic/DoubleType.v
+++ b/theories/Numbers/Cyclic/DoubleCyclic/DoubleType.v
@@ -53,7 +53,7 @@ Section Zn2Z.
End Zn2Z.
-Arguments W0 [znz].
+Arguments W0 {znz}.
(** From a cyclic representation [w], we iterate the [zn2z] construct
[n] times, gaining the type of binary trees of depth at most [n],