Changeset 1656


Ignore:
Timestamp:
Jan 23, 2012, 7:01:21 PM (6 years ago)
Author:
campbell
Message:

Minor fixups to RTLabs/Traces due to syntax changes.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/Traces.ma

    r1654 r1656  
    382382  >Estmt #LP whd in ⊢ (??%? → ?);
    383383  (* replace with lemma on successors? *)
    384   @bindIO_value #v #Ev @bindIO_value * #Eb whd in ⊢ (??%? → ?); #E destruct
     384  @bind_value #v #Ev @bind_ok * #Eb whd in ⊢ (??%? → ?); #E destruct
    385385  lapply (Hbody (next fr) (next_ok fr))
    386386  generalize in ⊢ (???% → ?);
     
    393393  >Estmt #LP whd in ⊢ (??%? → ?);
    394394  (* replace with lemma on successors? *)
    395   @bindIO_value #a cases a [ | #sz #i | #f | #r | #ptr ]  #Ea whd in ⊢ (??%? → ?);
     395  @bind_value #a cases a [ | #sz #i | #f | #r | #ptr ]  #Ea whd in ⊢ (??%? → ?);
    396396  [ 2: (* later *)
    397397  | *: #E destruct
     
    429429cases fd
    430430[ #fn whd in ⊢ (??%? → % → ?);
    431   @bindIO_value #lcl #Elcl cases (alloc m O (f_stacksize fn) Any)
     431  @bind_value #lcl #Elcl cases (alloc m O (f_stacksize fn) Any)
    432432  #m' #b whd in ⊢ (??%? → ?); #E' destruct
    433433  * whd in ⊢ (% → ?); * #WCL1 #WCL2 #WCL3
     
    435435| #fn whd in ⊢ (??%? → % → ?);
    436436  @bindIO_value #evargs #Eargs
    437   @bindIO_value #evres #Eres
    438   normalize in Eres; destruct
     437  whd in ⊢ (??%? → ?);
     438  #E' destruct
    439439] qed.
    440440
Note: See TracChangeset for help on using the changeset viewer.