diff options
| author |  Jason Gross <jgross@mit.edu> | 2018-09-18 15:45:21 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2018-09-18 15:45:21 -0400 |
| commit | 36b87035cd5db37e9c1fcd58e82376523cfd9a7d (patch) | |
| tree | 5218db53c10193342658811d9dd6d1ce2dad2fd2 /src/Util/PrimitiveSigma.v | |
| parent | 9d0f335bd50189239ed6770f4cde0949e27d0344 (diff) | |
Export notations when importing primitive
Diffstat (limited to 'src/Util/PrimitiveSigma.v')
| -rw-r--r-- | src/Util/PrimitiveSigma.v | 4 |
1 files changed, 1 insertions, 3 deletions
diff --git a/src/Util/PrimitiveSigma.v b/src/Util/PrimitiveSigma.v index 5a182e544..317f055a2 100644 --- a/src/Util/PrimitiveSigma.v +++ b/src/Util/PrimitiveSigma.v @@ -23,7 +23,7 @@ Module Import Primitive. Global Arguments projT1 {_ _} _. Global Arguments projT2 {_ _} _. - Module Import Notations. + Module Export Notations. Notation "{ x & P }" := (sigT (fun x => P)) : type_scope. Notation "{ x : A & P }" := (sigT (A:=A) (fun x => P)) : type_scope. Add Printing Let sigT. @@ -93,8 +93,6 @@ Notation "{ x & P }" := (sigT (fun x => P%primproj_type)) : primproj_type_scop Notation "{ x : A & P }" := (sigT (A:=A%primproj_type) (fun x => P%primproj_type)) : primproj_type_scope. Add Printing Let sigT. -Import Primitive.Notations. - Local Arguments f_equal {_ _} _ {_ _} _. Definition projT1_existT {A B} (a:A) (b:B a) : projT1 (existT B a b) = a := eq_refl. |