Ignore:
Timestamp:
Oct 14, 2011, 10:50:56 PM (9 years ago)
Author:
sacerdot
Message:
  • succ_pc generalized to return a res (necessary for LIN semantics)
  • succ_pc implemented for LIN
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/SemanticUtils.ma

    r1359 r1382  
    4040(*CSC: XXX This code is cut&paste from joint/semantics.ma, address_of_label.
    4141  Maybe there is a better way to organize the code!!! *)
    42 definition graph_succ_p: label → address → address.
     42definition graph_succ_p: label → address → res address.
    4343 #l #_ generalize in match (refl … (address_of_pointer (pointer_of_label l)))
    4444 cases (address_of_pointer (pointer_of_label l)) in ⊢ (???% → ?)
    45   [ #res #_ @res
    46   | #msg cases (pointer_of_label l) * * #q #com #off #E1 #E2 destruct normalize in E2; destruct ]
     45  [ #res #_ @(OK … res)
     46  | #msg cases (pointer_of_label l) * * #q #com #off #E1 destruct #E2 normalize in E2; destruct ]
    4747qed.
    4848
Note: See TracChangeset for help on using the changeset viewer.