Ignore:
Timestamp:
Jan 11, 2012, 5:41:45 PM (8 years ago)
Author:
tranquil
Message:
  • finished fork of semantics.ma
  • unification of Errors under the monad notations brings problems in type checking when res and IO are used together. Needs a lot of annotations, and may break the pre-fork material
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/TranslateUtils_paolo.ma

    r1635 r1640  
    104104  joint_internal_function globals dst_g_pars ≝
    105105  λsrc_g_pars,dst_g_pars,globals,registerT,fresh_reg,trans,empty,def.
    106   let f : label → joint_statement src_g_pars globals →
     106  let f : label → joint_statement (src_g_pars : params) globals →
    107107    joint_internal_function globals dst_g_pars → joint_internal_function globals dst_g_pars ≝
    108108    λlbl,stmt,def.
     
    128128  joint_internal_function … dst_g_pars ≝
    129129  λsrc_g_pars,dst_g_pars,globals,trans,empty,def.
    130   let f : label → joint_statement src_g_pars globals →
     130  let f : label → joint_statement (src_g_pars : params) globals →
    131131    joint_internal_function … dst_g_pars → joint_internal_function … dst_g_pars ≝
    132132    λlbl,stmt,def.
Note: See TracChangeset for help on using the changeset viewer.