Changeset 2184


Ignore:
Timestamp:
Jul 13, 2012, 7:59:41 PM (5 years ago)
Author:
campbell
Message:

Minor fix ups.

Location:
src
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/SimplifyCasts.ma

    r2176 r2184  
    30363036     whd in match (exec_step ??) in ⊢ (% → %);
    30373037     #Habsurd destruct (Habsurd)
    3038 ]
     3038] qed.
  • src/RTLabs/Traces.ma

    r2044 r2184  
    799799  >Estmt #LP whd in ⊢ (??%? → ?);
    800800  (* replace with lemma on successors? *)
    801   @bind_res_value #a cases a [ | #sz #i | #f | #r | #ptr ]  #Ea whd in ⊢ (??%? → ?);
     801  @bind_res_value #a cases a [ | #sz #i | #f | | #ptr ]  #Ea whd in ⊢ (??%? → ?);
    802802  [ 2: (* later *)
    803803  | *: #E destruct
     
    836836cases fd
    837837[ #fn whd in ⊢ (??%? → % → ?);
    838   @bind_res_value #lcl #Elcl cases (alloc m O (f_stacksize fn) Any)
     838  @bind_res_value #lcl #Elcl cases (alloc m O (f_stacksize fn) XData)
    839839  #m' #b whd in ⊢ (??%? → ?); #E' destruct
    840840  * whd in ⊢ (% → ?); * #WCL1 #WCL2 #WCL3
     
    14971497| #r #l1 #l2 #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev @bind_ok #b #Eb whd in ⊢ (??%? → ?); #E destruct %2 cases b [ %{l1} | %{l2} ] % // [ % | %2 %] //
    14981498| #r #ls #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev
    1499   cases v [ #E normalize in E; destruct | #sz #i | #f #E normalize in E; destruct | #r #E normalize in E; destruct | #p #E normalize in E; destruct ]
     1499  cases v [ #E normalize in E; destruct | #sz #i | #f #E normalize in E; destruct | #E normalize in E; destruct | #p #E normalize in E; destruct ]
    15001500  whd in ⊢ (??%? → ?);
    15011501  generalize in ⊢ (??(?%)? → ?);
     
    15891589| #r #l1 #l2 #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev @bind_ok #b #Eb whd in ⊢ (??%? → ?); #E destruct @refl
    15901590| #r #ls #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev
    1591   cases v [ #E normalize in E; destruct | #sz #i | #f #E normalize in E; destruct | #r #E normalize in E; destruct | #p #E normalize in E; destruct ]
     1591  cases v [ #E normalize in E; destruct | #sz #i | #f #E normalize in E; destruct | #E normalize in E; destruct | #p #E normalize in E; destruct ]
    15921592  whd in ⊢ (??%? → ?);
    15931593  generalize in ⊢ (??(?%)? → ?);
Note: See TracChangeset for help on using the changeset viewer.