Changeset 2177 for src/Clight/Csem.ma


Ignore:
Timestamp:
Jul 12, 2012, 2:56:50 PM (8 years ago)
Author:
campbell
Message:

Tidy up multiplication.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/Csem.ma

    r2176 r2177  
    197197      [ Vint sz1 n1 ⇒ match v2 with
    198198          [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1
    199                           (λn1. Some ? (Vint sz2 (\snd (vsplit ??? (multiplication ? n1 n2))))) (None ?)
     199                          (λn1. Some ? (Vint sz2 (short_multiplication ? n1 n2))) (None ?)
    200200        | _ ⇒ None ? ]
    201201      | _ ⇒ None ? ]
Note: See TracChangeset for help on using the changeset viewer.