aboutsummaryrefslogtreecommitdiff
path: root/src/Compilers/ZExtended/Syntax.v
diff options
context:
space:
mode:
authorGravatar Jason Gross <jgross@mit.edu>2017-10-22 01:19:35 -0400
committerGravatar Jason Gross <jgross@mit.edu>2017-10-22 01:19:35 -0400
commitd21545bd7d5c0eae64353a99f116bee18257f20a (patch)
treeddcf7d252e971d9c88c8be671fb84a966daecbac /src/Compilers/ZExtended/Syntax.v
parent72382e504b0f900f5180e2db3972a937676230f3 (diff)
Add ZExtended/InlineConstAndOp.v
Diffstat (limited to 'src/Compilers/ZExtended/Syntax.v')
-rw-r--r--src/Compilers/ZExtended/Syntax.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/src/Compilers/ZExtended/Syntax.v b/src/Compilers/ZExtended/Syntax.v
index 3d92e7b4e..5f6d5b3eb 100644
--- a/src/Compilers/ZExtended/Syntax.v
+++ b/src/Compilers/ZExtended/Syntax.v
@@ -74,4 +74,4 @@ Definition interp_op {s d} (opv : op s d) : interp_flat_type interp_base_type s
end.
Notation Expr := (Expr base_type op).
-Notation Interp := (Interp interp_op).
+Notation Interp := (Interp (@interp_op)).