diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-09-09 22:39:15 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-09-09 22:53:59 +0200 |
| commit | 0dd3f0d34873dcd126be8ec48724a310214f38ac (patch) | |
| tree | ccb5c83cba1db777681e8ecb7251dc486b3f2044 /theories/Numbers | |
| parent | e365fb8ffbbc62352a725de13cbf864b3fbb3840 (diff) | |
- Fix printing and parsing of primitive projections, including the Set
Printing All cases (bug #3597).
- Fix Ltac matching with primitive projections (bug #3598).
- Spotted a problem with printing of constants with maximally implicit
arguments due to strange "compatibility" interpretation of Arguments [X]
as Arguments {X} but didn't fix it entirely yet (might cause incompatibilities).
Diffstat (limited to 'theories/Numbers')
| -rw-r--r-- | theories/Numbers/Cyclic/DoubleCyclic/DoubleType.v | 2 |
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], |