diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/Compilers/Named/Syntax.v | 2 | ||||
| -rw-r--r-- | src/Compilers/Syntax.v | 2 |
2 files changed, 2 insertions, 2 deletions
diff --git a/src/Compilers/Named/Syntax.v b/src/Compilers/Named/Syntax.v index 993a5cc77..453e37de9 100644 --- a/src/Compilers/Named/Syntax.v +++ b/src/Compilers/Named/Syntax.v @@ -86,7 +86,7 @@ Global Arguments interp {_ _ _ _ _ interp_op ctx t} _ _. Global Arguments Interp {_ _ _ _ _ interp_op t} _ _. Notation "'nlet' x := A 'in' b" := (LetIn _ x A%nexpr b%nexpr) : nexpr_scope. -Notation "'nlet' x : tx := A 'in' b" := (LetIn tx x A%nexpr b%nexpr) : nexpr_scope. +Notation "'nlet' x : tx := A 'in' b" := (LetIn tx%ctype x%core A%nexpr b%nexpr) : nexpr_scope. Notation "'λn' x .. y , t" := (Abs x .. (Abs y t%nexpr) .. ) : nexpr_scope. Notation "( x , y , .. , z )" := (Pair .. (Pair x%nexpr y%nexpr) .. z%nexpr) : nexpr_scope. Notation "()" := TT : nexpr_scope. diff --git a/src/Compilers/Syntax.v b/src/Compilers/Syntax.v index 0e8f924da..78615162e 100644 --- a/src/Compilers/Syntax.v +++ b/src/Compilers/Syntax.v @@ -149,5 +149,5 @@ Module Export Notations. Notation "( )" := TT : expr_scope. Notation "()" := TT : expr_scope. Bind Scope ctype_scope with flat_type. - Bind Scope ctype_scope with type. + Bind Scope ctype_scope with ctype. End Notations. |