Changeset 882 for src/Clight/toCminor.ma


Ignore:
Timestamp:
Jun 3, 2011, 5:35:32 PM (9 years ago)
Author:
campbell
Message:

Fix up fragile proofs for current version of matita.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/toCminor.ma

    r881 r882  
    416416      match typ_of_type (typeof e1) return λx.CMexpr x → ? with
    417417      [ ASTptr r ⇒ λe1'.
    418           match access_mode ty return λx.access_mode ty = x → ? with
     418          match access_mode ty return λx.access_mode ty = x → res (CMexpr (typ_of_type ty)) with
    419419          [ By_value q ⇒ λ_.OK ? (Mem (typ_of_type ty) ? q e1')
    420420          | By_reference r' ⇒ λE. (region_should_eq r r' ? e1')⌈CMexpr (ASTptr r') ↦ CMexpr (typ_of_type ty)⌉
Note: See TracChangeset for help on using the changeset viewer.