Ignore:
Timestamp:
Mar 21, 2011, 6:27:22 PM (9 years ago)
Author:
campbell
Message:

Refine small-step executable semantics abstraction a little.
Some progress on using the new definition in CexecEquiv?, but only partial
because of over-eager normalisation by the destruct tactic.
Whole program semantics for RTLabs using it.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/RTLabs-syntax.ma

    r639 r702  
    22include "basics/logic.ma".
    33
    4 include "AST.ma".
    5 include "CostLabel.ma".
    6 include "FrontEndOps.ma".
    7 include "Registers.ma".
     4include "Clight/AST.ma".
     5include "Clight/CostLabel.ma".
     6include "common/FrontEndOps.ma".
     7include "common/Registers.ma".
    88
    9 include "cerco/Vector.ma".
    10 include "Graphs.ma".
     9include "ASM/Vector.ma".
     10include "common/Graphs.ma".
    1111
    1212(* XXX: ASTish stuff *)
Note: See TracChangeset for help on using the changeset viewer.