Ignore:
Timestamp:
Feb 21, 2013, 6:03:46 PM (7 years ago)
Author:
tranquil
Message:
  • in Arithmeticcs.ma: commented include that breaks script in latest matita
  • moved COST_LABEL out of joint_seq
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/TranslateUtils.ma

    r2681 r2688  
    414414    (f_fin l s)
    415415; f_step_on_cost :
    416   ∀l,c.f_step l (COST_LABEL … c) = bret … [ COST_LABEL … c ]
     416  ∀l,c.f_step l (COST_LABEL … c) =
     417    bret ? (step_block ??) 〈[ ], λ_.COST_LABEL dst globals c, [ ]〉
    417418}.
    418419
     
    426427    [ sequential s' nxt ⇒
    427428      match s' return λx.stmt_at ???? = Some ? (sequential … x nxt) → ? with
    428       [ step_seq s'' ⇒
    429         match s'' return λx.stmt_at ???? = Some ? (sequential … (step_seq … x) nxt) → ? with
    430         [ COST_LABEL c ⇒ λ_.〈c, nxt〉
    431         | _ ⇒ λabs.⊥
    432         ]
     429      [ COST_LABEL c ⇒ λ_.〈c, nxt〉
    433430      | _ ⇒ λabs.⊥
    434431      ]
Note: See TracChangeset for help on using the changeset viewer.