diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-05-14 11:47:00 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-05-14 11:47:00 -0400 |
| commit | 189a0eba8a2c8ddfbb27d92f2f461f21864815e3 (patch) | |
| tree | e71b29a3dd4d09ee36f99e22d342962ac5417dd3 /src/Compilers | |
| parent | f0aa1a484ecdc01c4aedd1a1ad75324619bc0456 (diff) | |
Fix some scoping
Diffstat (limited to 'src/Compilers')
| -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. |