diff options
| author | Chantal Keller <Chantal.Keller@lri.fr> | 2022-02-18 16:50:08 +0100 |
|---|---|---|
| committer | Chantal Keller <Chantal.Keller@lri.fr> | 2022-02-18 16:50:08 +0100 |
| commit | f01ad53d1cda7cf519eae137faa87ac47e8b3ab1 (patch) | |
| tree | 8027a135aa797c918fec3f29a9c1cc3a711e45b0 /src/State.v | |
| parent | cc1734c1bc641b0d00a34264c65bfb2604f7aea5 (diff) | |
| parent | 965520037392fa6c523348e3ff9dff5b9d5c2313 (diff) | |
| download | smtcoq-f01ad53d1cda7cf519eae137faa87ac47e8b3ab1.tar.gz smtcoq-f01ad53d1cda7cf519eae137faa87ac47e8b3ab1.zip | |
Merge remote-tracking branch 'origin/coq-8.12' into coq-8.13
Diffstat (limited to 'src/State.v')
| -rw-r--r-- | src/State.v | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/src/State.v b/src/State.v index 4e133c6..8b899f1 100644 --- a/src/State.v +++ b/src/State.v @@ -10,7 +10,7 @@ (**************************************************************************) -Require Import List Bool Int63 Psatz Ring63 PArray Omega Misc Ring. +Require Import List Bool Int63 Psatz Ring63 PArray Misc Ring. (* Require Import AxiomesInt. *) @@ -674,8 +674,8 @@ Module S. rewrite foldi_lt_r. apply C.resolve_correct; [ apply Hv | ring_simplify (i + 1 - 1); exact Hc ]. rewrite ltb_spec, to_Z_add_1_wB, to_Z_1. - rewrite leb_spec, to_Z_1 in Hi1; generalize (to_Z_bounded i); omega. - rewrite ltb_spec in Hi2; generalize (to_Z_bounded (length r)); omega. + rewrite leb_spec, to_Z_1 in Hi1; generalize (to_Z_bounded i); lia. + rewrite ltb_spec in Hi2; generalize (to_Z_bounded (length r)); lia. Qed. (* Weakening *) |