1 files changed, 2 insertions, 2 deletions
diff --git a/lib/Intv.v b/lib/Intv.v
index 4b5ed77d..3a491819 100644
--- a/lib/Intv.v
+++ b/lib/Intv.v
@@ -245,8 +245,8 @@ Next Obligation.
   red. lia.
 Qed.
 Next Obligation.
-  assert (x = hi - 1 \/ x < hi - 1) by lia.
-  destruct H2. congruence. auto.
+  assert (EITHER: x = hi - 1 \/ x < hi - 1) by lia.
+  destruct EITHER. congruence. auto.
 Qed.
 Next Obligation.
   exists wildcard'; split; auto. lia.