From 3ffda353b0d92ccd0ff3693ad0be81531c3c0537 Mon Sep 17 00:00:00 2001 From: xleroy Date: Wed, 9 Mar 2011 13:35:00 +0000 Subject: Updated for Coq 8.3pl1. Some cleanups in test/*/Makefile. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1597 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- lib/Intv.v | 5 +---- 1 file changed, 1 insertion(+), 4 deletions(-) (limited to 'lib/Intv.v') diff --git a/lib/Intv.v b/lib/Intv.v index 834f83d4..a8fbd714 100644 --- a/lib/Intv.v +++ b/lib/Intv.v @@ -248,16 +248,13 @@ Next Obligation. destruct H2. congruence. auto. Qed. Next Obligation. - elim wildcard'0. intros y [A B]. exists y; split; auto. omega. + exists wildcard'0; split; auto. omega. Qed. Next Obligation. exists (hi - 1); split; auto. omega. Qed. Next Obligation. omegaContradiction. -Qed. -Next Obligation. - apply Zwf_well_founded. Defined. End FORALL. -- cgit