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/PrimitiveProd.v | |
| parent | 9d0f335bd50189239ed6770f4cde0949e27d0344 (diff) | |
Export notations when importing primitive
Diffstat (limited to 'src/Util/PrimitiveProd.v')
| -rw-r--r-- | src/Util/PrimitiveProd.v | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/src/Util/PrimitiveProd.v b/src/Util/PrimitiveProd.v index 0e2748501..a22c08e78 100644 --- a/src/Util/PrimitiveProd.v +++ b/src/Util/PrimitiveProd.v @@ -21,7 +21,7 @@ Module Import Primitive. Global Arguments fst {_ _}. Global Arguments snd {_ _}. - Module Import Notations. + Module Export Notations. Notation "x * y" := (@prod x y) : type_scope. Notation "( x , y , .. , z )" := (pair .. (pair x y) .. z) : core_scope. End Notations. @@ -69,7 +69,6 @@ Module Import Primitive. End Primitive. Notation "x * y" := (@prod x%primproj_type y%primproj_type) : primproj_type_scope. Notation "( x , y , .. , z )" := (pair .. (pair x%primproj y%primproj) .. z%primproj) : primproj_scope. -Import Primitive.Notations. Local Arguments f_equal {_ _} _ {_ _} _. |