From f724ed1e270eb48060a510ff99219227c342ad6c Mon Sep 17 00:00:00 2001
From: Pierre Roux
Date: Thu, 31 Dec 2020 18:08:29 +0100
Subject: Fix #13579 (hnf on primitives raises an anomaly)

Also works for simpl.
---
 theories/Numbers/Cyclic/Int63/Int63.v | 1 +
 1 file changed, 1 insertion(+)

(limited to 'theories')

diff --git a/theories/Numbers/Cyclic/Int63/Int63.v b/theories/Numbers/Cyclic/Int63/Int63.v
index f324bbf52b..7bb725538b 100644
--- a/theories/Numbers/Cyclic/Int63/Int63.v
+++ b/theories/Numbers/Cyclic/Int63/Int63.v
@@ -954,6 +954,7 @@ Proof.
    intros _ HH; generalize (HH H1); discriminate.
  clear H.
  generalize (ltb_spec j i); case Int63.ltb; intros H2; unfold bit; simpl.
+   change 62%int63 with (digits - 1)%int63.
    assert (F2: (φ j < φ i)%Z) by (case H2; auto); clear H2.
    replace (is_zero (((x << i) >> j) << (digits - 1))) with true; auto.
    case (to_Z_bounded j); intros  H1j H2j.
-- 
cgit v1.2.3