From 0dd3f0d34873dcd126be8ec48724a310214f38ac Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Tue, 9 Sep 2014 22:39:15 +0200 Subject: - 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). --- theories/Numbers/Cyclic/DoubleCyclic/DoubleType.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'theories/Numbers') 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], -- cgit v1.2.3