diff options
Diffstat (limited to 'cfrontend/Csharpminor.v')
| -rw-r--r-- | cfrontend/Csharpminor.v | 9 |
1 files changed, 0 insertions, 9 deletions
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 := |