Changeset 225


Ignore:
Timestamp:
Nov 9, 2010, 12:52:32 PM (9 years ago)
Author:
campbell
Message:

Missing case in cast.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • C-semantics/CexecIO.ma

    r208 r225  
    164164[ true ⇒
    165165  match ty with
    166   [ Tpointer _ _ ⇒
     166  [ Tint _ _ ⇒
     167    match ty' with
     168    [ Tpointer _ _ ⇒ Some ? (OK ? (Vint i))
     169    | Tarray _ _ _ ⇒ Some ? (OK ? (Vint i))
     170    | Tfunction _ _ ⇒ Some ? (OK ? (Vint i))
     171    | _ ⇒ Some ? (Error ?)
     172    ]
     173  | Tpointer _ _ ⇒
    167174    match ty' with
    168175    [ Tpointer _ _ ⇒ Some ? (OK ? (Vint i))
     
    189196| false ⇒ Some ? (Error ?)
    190197]. nwhd; //; nlapply (eq_spec i zero); nrewrite > c0; #e; nrewrite > e;
    191    napply cast_pp_z; //; nqed.
     198   ##[ ##1,2,3: napply cast_ip_z ##| ##*: napply cast_pp_z ##] //; nqed.
    192199
    193200ndefinition ms_eq_dec : ∀s1,s2:memory_space. (s1 = s2) + (s1 ≠ s2).
Note: See TracChangeset for help on using the changeset viewer.