Changeset 1601 for src/RTL


Ignore:
Timestamp:
Dec 13, 2011, 2:49:52 PM (8 years ago)
Author:
sacerdot
Message:

Files ported to new version of the standard library.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTL/RTLToERTL.ma

    r1516 r1601  
    108108  let 〈def, tmpr〉 ≝ fresh_reg … def in
    109109  match reduce_strong ? ? RegisterSTS ret_regs with
    110   [ dp crl crl_proof ⇒
     110  [ mk_Sig crl crl_proof ⇒
    111111    let commonl ≝ \fst (\fst crl) in
    112112    let commonr ≝ \fst (\snd crl) in
     
    124124  λglobals.λstart_lbl: label.
    125125  match reduce_strong ? ? RegisterRets RegisterSTS with
    126   [ dp crl crl_proof ⇒
     126  [ mk_Sig crl crl_proof ⇒
    127127    let commonl ≝ \fst (\fst crl) in
    128128    let commonr ≝ \fst (\snd crl) in
     
    189189  λdef.
    190190  match fresh_regs_strong … globals def 2 with
    191   [ dp def_sra def_sra_proof ⇒
     191  [ mk_Sig def_sra def_sra_proof ⇒
    192192    let def ≝ \fst def_sra in
    193193    let sra ≝ \snd def_sra in
     
    256256  λstart_lbl: label.
    257257  match reduce_strong ? ? RegisterSTS RegisterRets with
    258   [ dp crl first_crl_proof ⇒
     258  [ mk_Sig crl first_crl_proof ⇒
    259259    let commonl ≝ \fst (\fst crl) in
    260260    let commonr ≝ \fst (\snd crl) in
     
    262262    let saves ≝ map2 ? ? ? f_save commonl commonr ? in
    263263    match reduce_strong ? ? ret_regs RegisterSTS with
    264     [ dp crl second_crl_proof ⇒
     264    [ mk_Sig crl second_crl_proof ⇒
    265265      let commonl ≝ \fst (\fst crl) in
    266266      let commonr ≝ \fst (\snd crl) in
Note: See TracChangeset for help on using the changeset viewer.