Changeset 309


Ignore:
Timestamp:
Nov 26, 2010, 1:12:40 AM (9 years ago)
Author:
sacerdot
Message:

assembly1 is finally compiling in about 37s!

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D4.1/Matita/Assembly.ma

    r308 r309  
    230230                              | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
    231231                          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1)]
    232                   | Right addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in [] (*
     232                  | Right addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
    233233                     let b1 ≝
    234234                      match addr1 return λx. bool_to_Prop (is_in ? [[direct]] x) → ? with
     
    240240                      | DIRECT b2 ⇒ λ_.[ ([[true;false;false;false;false;true;false;true]]); b1; b2 ]
    241241                      | INDIRECT i1 ⇒ λ_. [ ([[true;false;false;false;false;true;true;i1]]); b1 ]
    242                       | DATA b1 ⇒ λ_. [ ([[false;true;true;true;false;true;false;true]]); b1; b2 ]
    243                       | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)*)]
     242                      | DATA b2 ⇒ λ_. [ ([[false;true;true;true;false;true;false;true]]); b1; b2 ]
     243                      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)]
    244244              | Right addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
    245245                 match addr2 return λx. bool_to_Prop (is_in ? [[data16]] x) → ? with
Note: See TracChangeset for help on using the changeset viewer.