From 7ea8a55692e2a2d32efa0c84e19c37a3b56a0fd1 Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Fri, 19 Aug 2011 09:13:09 +0000
Subject: Cleaned up old commented-out parts

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1719 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
---
 cfrontend/Cexec.v | 14 --------------
 1 file changed, 14 deletions(-)

(limited to 'cfrontend/Cexec.v')

diff --git a/cfrontend/Cexec.v b/cfrontend/Cexec.v
index 383eeb8e..e3b57c51 100644
--- a/cfrontend/Cexec.v
+++ b/cfrontend/Cexec.v
@@ -1653,20 +1653,6 @@ Definition do_step (w: world) (s: state) : list (trace * state) :=
   | _ => nil
   end.
 
-(*
-Definition at_external (S: state): option (external_function * list val * mem) :=
-  match S with
-  | Callstate (External ef _ _) vargs k m => Some (ef, vargs, m)
-  | _ => None
-  end.
-
-Definition after_external (S: state) (v: val) (m: mem): option state :=
-  match S with
-  | Callstate _ _ k _ => Some (Returnstate v k m)
-  | _ => None
-  end.
-*)
-
 Ltac myinv :=
   match goal with
   | [ |- In _ nil -> _ ] => intro X; elim X
-- 
cgit