diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-05-05 22:47:26 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-05-05 22:47:26 +0000 |
| commit | 86a1787cf9ae815ee8b1f6fd7f39ac615da031a4 (patch) | |
| tree | 6b5a9ae23ea5bb3e15c9b517f781f6aa3df51133 /theories/Init/Specif.v | |
| parent | becc50a8ac662d666cbe2645d7d84a7ee7b0b8e4 (diff) | |
Relaxing the constraint on eta-expanding on the fly while looking for
notation to use at printing time. We now allow to print "sigT P" as
"{x:_ & P x}", generating a "_" for the missing type, when the notation
is defined by 'Notation "{ x : A & P }" := (sigT (fun x:A => P))'.
Do better, and change the notation to "(sigT (A:=A) (fun x => P))" so
that the type is known even when eta-expansion is needed.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16467 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Init/Specif.v')
| -rw-r--r-- | theories/Init/Specif.v | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/theories/Init/Specif.v b/theories/Init/Specif.v index 6adc1c369..88c2c264a 100644 --- a/theories/Init/Specif.v +++ b/theories/Init/Specif.v @@ -45,11 +45,11 @@ Arguments sigT2 (A P Q)%type. Notation "{ x | P }" := (sig (fun x => P)) : type_scope. Notation "{ x | P & Q }" := (sig2 (fun x => P) (fun x => Q)) : type_scope. -Notation "{ x : A | P }" := (sig (fun x:A => P)) : type_scope. -Notation "{ x : A | P & Q }" := (sig2 (fun x:A => P) (fun x:A => Q)) : +Notation "{ x : A | P }" := (sig (A:=A) (fun x => P)) : type_scope. +Notation "{ x : A | P & Q }" := (sig2 (A:=A) (fun x => P) (fun x => Q)) : type_scope. -Notation "{ x : A & P }" := (sigT (fun x:A => P)) : type_scope. -Notation "{ x : A & P & Q }" := (sigT2 (fun x:A => P) (fun x:A => Q)) : +Notation "{ x : A & P }" := (sigT (A:=A) (fun x => P)) : type_scope. +Notation "{ x : A & P & Q }" := (sigT2 (A:=A) (fun x => P) (fun x => Q)) : type_scope. Add Printing Let sig. |