Ignore:
Timestamp:
Feb 18, 2013, 5:48:19 PM (7 years ago)
Author:
tranquil
Message:
  • another change in block definition
  • RTLabs -> RTL and ERTL -> ERTLptr passes fixed, others stil broken
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ERTLptr/ERTLptr.ma

    r2645 r2674  
    2020    (* call_dest ≝ *) unit
    2121    (* ext_seq ≝ *) ertlptr_seq
    22     (* ext_seq_labels ≝ *) (λ_.[])
     22    (* ext_seq_labels ≝ *)
     23      (λs.match s with [ LOW_ADDRESS _ l ⇒ [l] | HIGH_ADDRESS _ l ⇒ [l] | _ ⇒ [ ]])
    2324    (* has_tailcall ≝ *) false
    2425    (* paramsT ≝ *) ℕ.
Note: See TracChangeset for help on using the changeset viewer.