diff options
Diffstat (limited to 'theories/Numbers/Cyclic')
| -rw-r--r-- | theories/Numbers/Cyclic/Abstract/CyclicAxioms.v | 2 | ||||
| -rw-r--r-- | theories/Numbers/Cyclic/DoubleCyclic/DoubleType.v | 2 |
2 files changed, 2 insertions, 2 deletions
diff --git a/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v b/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v index 3aa0753840..59656eedbe 100644 --- a/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v +++ b/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v @@ -204,7 +204,7 @@ Module ZnZ. End Specs. - Implicit Arguments Specs [[t]]. + Arguments Specs {t} ops. (** Generic construction of double words *) diff --git a/theories/Numbers/Cyclic/DoubleCyclic/DoubleType.v b/theories/Numbers/Cyclic/DoubleCyclic/DoubleType.v index 073afec37b..a274b8395b 100644 --- a/theories/Numbers/Cyclic/DoubleCyclic/DoubleType.v +++ b/theories/Numbers/Cyclic/DoubleCyclic/DoubleType.v @@ -53,7 +53,7 @@ Section Zn2Z. End Zn2Z. -Implicit 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], |