Ignore:
Timestamp:
Feb 23, 2013, 5:05:03 PM (7 years ago)
Author:
campbell
Message:

It's easier to keep the real function identifier in front-end Callstates
than mucking around with the function pointer.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/CexecComplete.ma

    r2677 r2722  
    362362    change with (store_value_of_type' (typeof e) m 〈loc,ofs〉 v) in H3:(??%?);
    363363    >H3 @refl
    364 | #f #e #eargs #k #ef #m #vf #vargs #f' #tr1 #tr2 #H1 #H2 #H3 #H4 whd in ⊢ (??%?);
     364| #f #e #eargs #k #ef #m #vf #vargs #f' #fid #tr1 #tr2 #H1 #H2 #H3 #H4 whd in ⊢ (??%?);
    365365    >(yields_eq ??? (expr_complete … H1)) whd in ⊢ (??%?);
    366366    >(yields_eq ??? (exprlist_complete … H2)) whd in ⊢ (??%?);
     
    368368    >H4 elim (assert_type_eq_true (fun_typeof e)); #pty #ety >ety
    369369    @refl
    370 | #f #el #ef #eargs #k #env #m #loc #ofs #vf #vargs #f' #tr1 #tr2 #tr3 #H1 #H2 #H3 #H4 #H5 whd in ⊢ (??%?);
     370| #f #el #ef #eargs #k #env #m #loc #ofs #vf #vargs #f' #fid #tr1 #tr2 #tr3 #H1 #H2 #H3 #H4 #H5 whd in ⊢ (??%?);
    371371    >(yields_eq ??? (expr_complete … H2)) whd in ⊢ (??%?);
    372372    >(yields_eq ??? (exprlist_complete … H3)) whd in ⊢ (??%?);
Note: See TracChangeset for help on using the changeset viewer.