Changeset 3048


Ignore:
Timestamp:
Apr 1, 2013, 12:06:07 AM (4 years ago)
Author:
campbell
Message:

Improve dependency for cast simplification.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/SimplifyCasts.ma

    r2722 r3048  
    55include "Clight/Cexec.ma".
    66include "Clight/casts.ma".
    7 include "Clight/CexecSound.ma".
     7include "Clight/CexecInd.ma".
    88
    99include "Clight/frontend_misc.ma".
     
    19061906
    19071907
    1908 definition expr_lvalue_ind_combined ≝
    1909 λP,Q,ci,lv,vr,dr,ao,uo,bo,ca,cd,ab,ob,sz,fl,co,xx.
    1910 conj ??
    1911  (expr_lvalue_ind P Q ci lv vr dr ao uo bo ca cd ab ob sz fl co xx)
    1912  (lvalue_expr_ind P Q ci lv vr dr ao uo bo ca cd ab ob sz fl co xx).
    1913  
    19141908lemma simulation_transitive : ∀A,r0,r1,r2. res_sim A r0 r1 → res_sim A r1 r2 → res_sim A r0 r2.
    19151909#A #r0 #r1 #r2 *
Note: See TracChangeset for help on using the changeset viewer.