diff options
| author | Matthieu Sozeau | 2014-09-09 22:39:15 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2014-09-09 22:53:59 +0200 |
| commit | 0dd3f0d34873dcd126be8ec48724a310214f38ac (patch) | |
| tree | ccb5c83cba1db777681e8ecb7251dc486b3f2044 /theories/Init | |
| 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/Init')
| -rw-r--r-- | theories/Init/Datatypes.v | 4 | ||||
| -rw-r--r-- | theories/Init/Specif.v | 2 |
2 files changed, 3 insertions, 3 deletions
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 *) |