From a0a5ac6bdf9450a57c2306aeda4b4add980c79bd Mon Sep 17 00:00:00 2001
From: letouzey <letouzey@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Thu, 16 Feb 2006 23:39:35 +0000
Subject: PL: Un mot-cle Proof qui n'a rien a faire la...

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@5 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
---
 backend/PPCgenproof.v | 1 -
 1 file changed, 1 deletion(-)

diff --git a/backend/PPCgenproof.v b/backend/PPCgenproof.v
index d89046fd..99aa4c83 100644
--- a/backend/PPCgenproof.v
+++ b/backend/PPCgenproof.v
@@ -97,7 +97,6 @@ Fixpoint code_tail (pos: Z) (c: code) {struct c} : code :=
   | nil => nil
   | i :: il => if zeq pos 0 then c else code_tail (pos - 1) il
   end.
-Proof.
 
 Lemma find_instr_tail:
   forall c pos,
-- 
cgit