Changeset 2688 for src/ERTLptr


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/ERTLptr/ERTLtoERTLptr.ma

    r2681 r2688  
    2222match s with
    2323[COMMENT s ⇒ COMMENT ERTLptr … s
    24 |COST_LABEL c ⇒ COST_LABEL ERTLptr … c
    2524|MOVE a  ⇒ MOVE ERTLptr … a
    2625|POP a ⇒ POP ERTLptr … a
     
    5453        λ_.CALL ERTLptr ? (inr … dest1) args dest, [ ]〉
    5554    ]
     55|COST_LABEL c ⇒ bret … 〈[ ], λ_.COST_LABEL ERTLptr … c, [ ]〉
    5656| COND reg l ⇒ bret … 〈[ ], λ_.COND ERTLptr ? reg l, [ ]〉
    5757| step_seq x ⇒ bret … [seq_embed … x]
     
    9191| whd %{I I}
    9292| #abs #called #args whd %{I I}
     93| #c %{I} %{I} #l %
    9394| * #called #args #dest whd in match translate_step; normalize nodelta whd
    9495  [ %{I} %{I} #l %
Note: See TracChangeset for help on using the changeset viewer.