From 72af7655d9227fcba3949a2a9d9e39d5116a568a Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Thu, 27 Oct 2016 13:54:22 -0400 Subject: Make it easier to export only phoas notations --- src/Reflection/Syntax.v | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) (limited to 'src') diff --git a/src/Reflection/Syntax.v b/src/Reflection/Syntax.v index ccdceb16f..af6ab3e20 100644 --- a/src/Reflection/Syntax.v +++ b/src/Reflection/Syntax.v @@ -273,6 +273,8 @@ Global Arguments interp {_ _ _} interp_op {t} _. Global Arguments interpf {_ _ _} interp_op {t} _. Global Arguments invert_Const {_ _ _ _ _} _. -Notation "'slet' x := A 'in' b" := (LetIn A (fun x => b)) : expr_scope. -Notation "'λ' x .. y , t" := (Abs (fun x => .. (Abs (fun y => t%expr)) ..)) : expr_scope. -Notation "( x , y , .. , z )" := (Pair .. (Pair x%expr y%expr) .. z%expr) : expr_scope. +Module Export Notations. + Notation "'slet' x := A 'in' b" := (LetIn A (fun x => b)) : expr_scope. + Notation "'λ' x .. y , t" := (Abs (fun x => .. (Abs (fun y => t%expr)) ..)) : expr_scope. + Notation "( x , y , .. , z )" := (Pair .. (Pair x%expr y%expr) .. z%expr) : expr_scope. +End Notations. -- cgit v1.2.3