Ignore:
Timestamp:
Oct 11, 2011, 6:00:03 PM (8 years ago)
Author:
sacerdot
Message:
  1. more work on the RTL semantics
  2. changes to joint/semantics to accomodate the RTL one
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/SemanticUtils.ma

    r1329 r1359  
    11include "joint/semantics.ma".
     2include alias "common/Identifiers.ma".
    23
    34(*** Store/retrieve on pseudo-registers ***)
     
    4344 cases (address_of_pointer (pointer_of_label l)) in ⊢ (???% → ?)
    4445  [ #res #_ @res
    45   | #msg cases (pointer_of_label l) * * #q #com #off #E1 #E2 destruct ]
     46  | #msg cases (pointer_of_label l) * * #q #com #off #E1 #E2 destruct normalize in E2; destruct ]
    4647qed.
    4748
Note: See TracChangeset for help on using the changeset viewer.