Fix for Coq 8.4

1 files changed, 3 insertions, 3 deletions

diff --git a/src/Reflection/Z/Interpretations.v b/src/Reflection/Z/Interpretations.v
index 26ce02e03..0da74da09 100644
--- a/src/Reflection/Z/Interpretations.v
+++ b/src/Reflection/Z/Interpretations.v
@@ -406,9 +406,9 @@ Module ZBounds.
     : Tuple.tuple t (S pred_n)
     := Tuple.push_option
          match int_width, Tuple.lift_option modulus, Tuple.lift_option value with
-         | Some int_width, Some modulus, Some value
-           => if check_conditional_subtract_bounds pred_n int_width modulus value
-              then Some (conditional_subtract' pred_n int_width modulus value)
+         | Some int_width, Some modulus, Some value'
+           => if check_conditional_subtract_bounds pred_n int_width modulus value'
+              then Some (conditional_subtract' pred_n int_width modulus value')
               else None
          | _, _, _ => None
          end.