aboutsummaryrefslogtreecommitdiff
path: root/src/Compilers/ZExtended/Syntax.v
diff options
context:
space:
mode:
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)).