From 6f3225b0623b9c97eed7d40ddc320b08c79c6518 Mon Sep 17 00:00:00 2001 From: xleroy Date: Sun, 10 Feb 2013 10:08:27 +0000 Subject: lib/Integers.v: revised and extended, faster implementation based on bit-level operations provided by ZArith in Coq 8.4. Other modules: adapted accordingly. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2110 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- cfrontend/SimplExprspec.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'cfrontend/SimplExprspec.v') diff --git a/cfrontend/SimplExprspec.v b/cfrontend/SimplExprspec.v index 5cb0f189..b31738b5 100644 --- a/cfrontend/SimplExprspec.v +++ b/cfrontend/SimplExprspec.v @@ -591,7 +591,7 @@ Lemma within_widen: Proof. intros. destruct H. split. eapply Ple_trans; eauto. - unfold Plt, Ple in *. omega. + eapply Plt_Ple_trans; eauto. Qed. Definition contained (l: list ident) (g1 g2: generator) : Prop := -- cgit