diff options
| -rw-r--r-- | backend/PPCgenproof.v | 1 |
1 files changed, 0 insertions, 1 deletions
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, |