aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--src/Compilers/CommonSubexpressionEliminationDenote.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/src/Compilers/CommonSubexpressionEliminationDenote.v b/src/Compilers/CommonSubexpressionEliminationDenote.v
index c45fae00e..2218f62eb 100644
--- a/src/Compilers/CommonSubexpressionEliminationDenote.v
+++ b/src/Compilers/CommonSubexpressionEliminationDenote.v
@@ -58,7 +58,7 @@ Section symbolic.
:= match se, t with
| STT, Unit => Some tt
| SVar n, t
- => match List.nth_error m (length m - n) with
+ => match List.nth_error m (length m - S n) with
| Some e => @var_cast _ t (projT2 (snd e))
| None => None
end