From 36b87035cd5db37e9c1fcd58e82376523cfd9a7d Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Tue, 18 Sep 2018 15:45:21 -0400 Subject: Export notations when importing primitive --- src/Util/PrimitiveProd.v | 3 +-- src/Util/PrimitiveSigma.v | 4 +--- 2 files changed, 2 insertions(+), 5 deletions(-) (limited to 'src/Util') 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 {_ _} _ {_ _} _. 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. -- cgit v1.2.3