aboutsummaryrefslogtreecommitdiffstats
path: root/cfrontend/Cminorgen.v
diff options
context:
space:
mode:
authorYann Herklotz <git@yannherklotz.com>2021-09-17 18:28:55 +0100
committerYann Herklotz <git@yannherklotz.com>2021-09-17 18:28:55 +0100
commita1c401a4eba5fc9fcf42933f70005ecb679a4c1c (patch)
tree26637fca5d1da9b3d049234721d593a60b03a6d3 /cfrontend/Cminorgen.v
parentc49caca4b5f0239b43610fbfe012d6ba0211b364 (diff)
parent1daf96cdca4d828c333cea5c9a314ef861342984 (diff)
downloadcompcert-a1c401a4eba5fc9fcf42933f70005ecb679a4c1c.tar.gz
compcert-a1c401a4eba5fc9fcf42933f70005ecb679a4c1c.zip
Merge branch 'master' into dev/michalisdev/michalis
Diffstat (limited to 'cfrontend/Cminorgen.v')
-rw-r--r--cfrontend/Cminorgen.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/cfrontend/Cminorgen.v b/cfrontend/Cminorgen.v
index 45c21f96..1b031866 100644
--- a/cfrontend/Cminorgen.v
+++ b/cfrontend/Cminorgen.v
@@ -240,7 +240,7 @@ Module VarOrder <: TotalLeBool.
Theorem leb_total: forall v1 v2, leb v1 v2 = true \/ leb v2 v1 = true.
Proof.
unfold leb; intros.
- assert (snd v1 <= snd v2 \/ snd v2 <= snd v1) by omega.
+ assert (snd v1 <= snd v2 \/ snd v2 <= snd v1) by lia.
unfold proj_sumbool. destruct H; [left|right]; apply zle_true; auto.
Qed.
End VarOrder.