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/FSets/FMapPositive.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'theories/FSets') diff --git a/theories/FSets/FMapPositive.v b/theories/FSets/FMapPositive.v index c9d868c40..3eac15b03 100644 --- a/theories/FSets/FMapPositive.v +++ b/theories/FSets/FMapPositive.v @@ -82,7 +82,7 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits. Section A. Variable A:Type. - Arguments Leaf [A]. + Arguments Leaf {A}. Definition empty : t A := Leaf. @@ -812,7 +812,7 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits. Variable A B C : Type. Variable f : option A -> option B -> option C. - Arguments Leaf [A]. + Arguments Leaf {A}. Fixpoint xmap2_l (m : t A) : t C := match m with -- cgit v1.2.3