From 00b605a1d52696b055dd232a05dd54a312680b93 Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Thu, 26 Mar 2009 09:50:18 +0000
Subject: Added tail call optimization pass

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

(limited to 'backend/RTLtyping.v')

diff --git a/backend/RTLtyping.v b/backend/RTLtyping.v
index 60b1d72c..f466a90c 100644
--- a/backend/RTLtyping.v
+++ b/backend/RTLtyping.v
@@ -167,12 +167,6 @@ Section TYPECHECKING.
 Variable funct: function.
 Variable env: regenv.
 
-Lemma typ_eq: forall (t1 t2: typ), {t1=t2} + {t1<>t2}.
-Proof. decide equality. Qed.
-
-Lemma opt_typ_eq: forall (t1 t2: option typ), {t1=t2} + {t1<>t2}.
-Proof. decide equality. apply typ_eq. Qed.
-
 Definition check_reg (r: reg) (ty: typ): bool :=
   if typ_eq (env r) ty then true else false.
 
-- 
cgit