diff options
author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2011-08-19 09:13:09 +0000 |
---|---|---|
committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2011-08-19 09:13:09 +0000 |
commit | 7ea8a55692e2a2d32efa0c84e19c37a3b56a0fd1 (patch) | |
tree | e324aff1a958e0a5d83f805ff3ca1d9eb07939f4 /cfrontend/Cexec.v | |
parent | 5b73a4f223a0cadb7df3f1320fed86cde0d67d6e (diff) | |
download | compcert-7ea8a55692e2a2d32efa0c84e19c37a3b56a0fd1.tar.gz compcert-7ea8a55692e2a2d32efa0c84e19c37a3b56a0fd1.zip |
Cleaned up old commented-out parts
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1719 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'cfrontend/Cexec.v')
-rw-r--r-- | cfrontend/Cexec.v | 14 |
1 files changed, 0 insertions, 14 deletions
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 |