Ignore:
Timestamp:
Feb 7, 2013, 10:43:49 PM (7 years ago)
Author:
sacerdot
Message:

...

File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/frontEndMem.ml

    r2601 r2649  
    1010
    1111open Deqsets
     12
     13open ErrorMessages
    1214
    1315open PreIdentifiers
     
    2527open Identifiers
    2628
    27 open Coqlib
    28 
    29 open Floats
    30 
    3129open Integers
    3230
     
    3634
    3735open Arithmetic
    38 
    39 open Char
    40 
    41 open String
    4236
    4337open Extranat
     
    8680
    8781open GenMem
     82
     83open Coqlib
    8884
    8985open Values
     
    160156  Bool.andb
    161157    (Bool.andb
    162       (Z.zltb ptr.Pointers.pblock.Pointers.block_id m.GenMem.nextblock)
     158      (Z.zltb (Pointers.block_id ptr.Pointers.pblock) m.GenMem.nextblock)
    163159      (Z.zleb (GenMem.low_bound m ptr.Pointers.pblock) off))
    164160    (Z.zltb off (GenMem.high_bound m ptr.Pointers.pblock))
Note: See TracChangeset for help on using the changeset viewer.