Adapt w.r.t. coq/coq#15442 (#425)

coq/coq#15442 changes the way `Program` names things, to make it uniform w.r.t. the standard naming schema.

This commit removes dependencies on the names chosen by `Program`.  Should be backwards compatible.

Co-authored-by: Xavier Leroy <xavier.leroy@college-de-france.fr>

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.