diff options
Diffstat (limited to 'theories/Init/Specif.v')
| -rw-r--r-- | theories/Init/Specif.v | 45 |
1 files changed, 28 insertions, 17 deletions
diff --git a/theories/Init/Specif.v b/theories/Init/Specif.v index c42cc00b8..b6afba29a 100644 --- a/theories/Init/Specif.v +++ b/theories/Init/Specif.v @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (** Basic specifications : sets that may contain logical information *) @@ -54,6 +56,15 @@ 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. +Notation "{ ' pat | P }" := (sig (fun pat => P)) : type_scope. +Notation "{ ' pat | P & Q }" := (sig2 (fun pat => P) (fun pat => Q)) : type_scope. +Notation "{ ' pat : A | P }" := (sig (A:=A) (fun pat => P)) : type_scope. +Notation "{ ' pat : A | P & Q }" := (sig2 (A:=A) (fun pat => P) (fun pat => Q)) : + type_scope. +Notation "{ ' pat : A & P }" := (sigT (A:=A) (fun pat => P)) : type_scope. +Notation "{ ' pat : A & P & Q }" := (sigT2 (A:=A) (fun pat => P) (fun pat => Q)) : + type_scope. + Add Printing Let sig. Add Printing Let sig2. Add Printing Let sigT. @@ -734,16 +745,16 @@ Hint Resolve exist exist2 existT existT2: core. (* Compatibility *) -Notation sigS := sigT (compat "8.2"). -Notation existS := existT (compat "8.2"). -Notation sigS_rect := sigT_rect (compat "8.2"). -Notation sigS_rec := sigT_rec (compat "8.2"). -Notation sigS_ind := sigT_ind (compat "8.2"). -Notation projS1 := projT1 (compat "8.2"). -Notation projS2 := projT2 (compat "8.2"). - -Notation sigS2 := sigT2 (compat "8.2"). -Notation existS2 := existT2 (compat "8.2"). -Notation sigS2_rect := sigT2_rect (compat "8.2"). -Notation sigS2_rec := sigT2_rec (compat "8.2"). -Notation sigS2_ind := sigT2_ind (compat "8.2"). +Notation sigS := sigT (compat "8.6"). +Notation existS := existT (compat "8.6"). +Notation sigS_rect := sigT_rect (compat "8.6"). +Notation sigS_rec := sigT_rec (compat "8.6"). +Notation sigS_ind := sigT_ind (compat "8.6"). +Notation projS1 := projT1 (compat "8.6"). +Notation projS2 := projT2 (compat "8.6"). + +Notation sigS2 := sigT2 (compat "8.6"). +Notation existS2 := existT2 (compat "8.6"). +Notation sigS2_rect := sigT2_rect (compat "8.6"). +Notation sigS2_rec := sigT2_rec (compat "8.6"). +Notation sigS2_ind := sigT2_ind (compat "8.6"). |