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/Csharpminor.v | 9 ---------
 1 file changed, 9 deletions(-)

(limited to 'cfrontend/Csharpminor.v')

diff --git a/cfrontend/Csharpminor.v b/cfrontend/Csharpminor.v
index c192e463..a1ed8b33 100644
--- a/cfrontend/Csharpminor.v
+++ b/cfrontend/Csharpminor.v
@@ -416,15 +416,6 @@ Inductive exec_assign: env -> mem -> ident -> val -> mem -> Prop :=
     Mem.store chunk m b 0 v = Some m' ->
     exec_assign e m id v m'.
 
-(*
-Inductive exec_opt_assign: env -> mem -> option ident -> val -> mem -> Prop :=
-  | exec_assign_none: forall e m v,
-      exec_opt_assign e m None v m
-  | exec_assign_some: forall e m id v m',
-      exec_assign e m id v m' ->
-      exec_opt_assign e m (Some id) v m'.
-*)
-
 (** One step of execution *)
 
 Inductive step: state -> trace -> state -> Prop :=
-- 
cgit