aboutsummaryrefslogtreecommitdiff
path: root/src/Compilers/Named/InterpretToPHOAS.v
diff options
context:
space:
mode:
Diffstat (limited to 'src/Compilers/Named/InterpretToPHOAS.v')
-rw-r--r--src/Compilers/Named/InterpretToPHOAS.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/src/Compilers/Named/InterpretToPHOAS.v b/src/Compilers/Named/InterpretToPHOAS.v
index 1ccad6cad..4e74fc59a 100644
--- a/src/Compilers/Named/InterpretToPHOAS.v
+++ b/src/Compilers/Named/InterpretToPHOAS.v
@@ -27,7 +27,7 @@ Module Export Named.
: @Syntax.exprf base_type_code op var t
:= match e in Named.exprf _ _ _ t return @Syntax.exprf base_type_code op var t with
| Named.Var t' x
- => match lookupb ctx x t' with
+ => match lookupb t' ctx x with
| Some v => Var v
| None => failf _
end