Changeset 1938 for src/ASM/Interpret.ma


Ignore:
Timestamp:
May 14, 2012, 10:05:36 AM (8 years ago)
Author:
sacerdot
Message:

Definitions moved to the right places, now everything compiles again.

File:
1 edited

Legend:

Unmodified
Added
Removed

  • src/ASM/Interpret.ma

    r1935 r1938  
    22include "ASM/StatusProofs.ma".
    33include "ASM/Fetch.ma".
     4include "common/StructuredTraces.ma".
    45
    56definition sign_extension: Byte → Word ≝
    … …  
    119120include alias "arithmetics/nat.ma".
    120121include alias "ASM/BitVectorTrie.ma".
    121 
    122 inductive status_class : Type[0] ≝
    123 | cl_return : status_class
    124 | cl_jump   : status_class
    125 | cl_call   : status_class
    126 | cl_other : status_class.
    127122
    128123definition ASM_classify00: ∀a. preinstruction a → status_class ≝
Note: See TracChangeset for help on using the changeset viewer.