Changeset 2665


Ignore:
Timestamp:
Feb 14, 2013, 10:01:35 AM (7 years ago)
Author:
sacerdot
Message:

...

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/ASMCostsSplit.ma

    r2657 r2665  
    337337  λl_sig.
    338338  lookup_present … cost_map (as_cost_get_label ? l_sig) ?.
    339   cases cost_map
    340   #m * #prf #_ cases l_sig cases daemon (*bla bla*)
    341   qed.
     339  cases cost_map #m * #prf #_ cases l_sig
     340  #l * #pc #Hl whd in Hl; whd whd in match (as_cost_get_label ??);
     341  whd in Hl:(??%?); lapply (prf … Hl) //
     342qed.
Note: See TracChangeset for help on using the changeset viewer.