aboutsummaryrefslogtreecommitdiff
path: root/src/Compilers/Named/Syntax.v
diff options
context:
space:
mode:
Diffstat (limited to 'src/Compilers/Named/Syntax.v')
-rw-r--r--src/Compilers/Named/Syntax.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/src/Compilers/Named/Syntax.v b/src/Compilers/Named/Syntax.v
index 453e37de9..34ba1f48f 100644
--- a/src/Compilers/Named/Syntax.v
+++ b/src/Compilers/Named/Syntax.v
@@ -44,7 +44,7 @@ Module Export Named.
(ctx : Context) {t} (e : exprf t)
: option (interp_flat_type t)
:= match e in exprf t return option (interp_flat_type t) with
- | Var t' x => lookupb ctx x t'
+ | Var t' x => lookupb t' ctx x
| TT => Some tt
| Pair _ ex _ ey
=> match @interpf ctx _ ex, @interpf ctx _ ey with