- 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).

4 files changed, 6 insertions, 6 deletions

diff --git a/theories/FSets/FMapPositive.v b/theories/FSets/FMapPositive.v
index c9d868c40f..3eac15b038 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
diff --git a/theories/Init/Datatypes.v b/theories/Init/Datatypes.v
index c8d18f7661..093a2c1407 100644
--- a/theories/Init/Datatypes.v
+++ b/theories/Init/Datatypes.v
@@ -151,7 +151,7 @@ Inductive option (A:Type) : Type :=
   | Some : A -> option A
   | None : option A.
 
-Arguments None [A].
+Arguments None {A}.
 
 Definition option_map (A B:Type) (f:A->B) (o : option A) : option B :=
   match o with
@@ -224,7 +224,7 @@ Inductive list (A : Type) : Type :=
  | nil : list A
  | cons : A -> list A -> list A.
 
-Arguments nil [A].
+Arguments nil {A}.
 Infix "::" := cons (at level 60, right associativity) : list_scope.
 Delimit Scope list_scope with list.
 Bind Scope list_scope with list.
diff --git a/theories/Init/Specif.v b/theories/Init/Specif.v
index 1ddb59cf45..c3edcfdfd7 100644
--- a/theories/Init/Specif.v
+++ b/theories/Init/Specif.v
@@ -285,7 +285,7 @@ Section Exc.
   Definition value := @Some A.
   Definition error := @None A.
 End Exc.
-Arguments error [A].
+Arguments error {A}.
 
 Definition except := False_rec. (* for compatibility with previous versions *)
 
diff --git a/theories/Numbers/Cyclic/DoubleCyclic/DoubleType.v b/theories/Numbers/Cyclic/DoubleCyclic/DoubleType.v
index ce1c0bef1b..900cb1db50 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],