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

...

File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/globalenvs.mli

    r2601 r2649  
    11open Preamble
    22
     3open ErrorMessages
     4
    35open Option
    46
     
    1315open Positive
    1416
    15 open Char
    16 
    17 open String
    18 
    1917open PreIdentifiers
    2018
     
    5149open Identifiers
    5250
     51open Arithmetic
     52
     53open Vector
     54
     55open Div_and_mod
     56
     57open Util
     58
     59open FoldStuff
     60
     61open BitVector
     62
     63open Extranat
     64
     65open Integers
     66
     67open AST
     68
    5369open Coqlib
    54 
    55 open Floats
    56 
    57 open Arithmetic
    58 
    59 open Vector
    60 
    61 open Div_and_mod
    62 
    63 open Util
    64 
    65 open FoldStuff
    66 
    67 open BitVector
    68 
    69 open Extranat
    70 
    71 open Integers
    72 
    73 open AST
    7470
    7571open Values
     
    177173
    178174val size_init_data_list : AST.init_data List.list -> Nat.nat
    179 
    180 val initDataStoreFailed : String.string
    181175
    182176val add_globals :
     
    216210
    217211val alloc_pair :
    218   GenMem.mem1 -> GenMem.mem1 -> Z.z -> Z.z -> Z.z -> Z.z -> AST.region ->
    219   (GenMem.mem1 -> GenMem.mem1 -> Pointers.block Types.sig0 -> __ -> 'a1) ->
    220   'a1
     212  GenMem.mem1 -> GenMem.mem1 -> Z.z -> Z.z -> Z.z -> Z.z -> (GenMem.mem1 ->
     213  GenMem.mem1 -> Pointers.block -> __ -> 'a1) -> 'a1
    221214
    222215val prod_jmdiscr0 : ('a1, 'a2) Types.prod -> ('a1, 'a2) Types.prod -> __
     
    265258
    266259val related_globals_gen_rect_Type4 :
    267   String.string -> (Identifiers.universe -> 'a1 -> ('a2,
     260  PreIdentifiers.identifierTag -> (Identifiers.universe -> 'a1 -> ('a2,
    268261  Identifiers.universe) Types.prod) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __
    269262  -> __ -> 'a3) -> 'a3
    270263
    271264val related_globals_gen_rect_Type5 :
    272   String.string -> (Identifiers.universe -> 'a1 -> ('a2,
     265  PreIdentifiers.identifierTag -> (Identifiers.universe -> 'a1 -> ('a2,
    273266  Identifiers.universe) Types.prod) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __
    274267  -> __ -> 'a3) -> 'a3
    275268
    276269val related_globals_gen_rect_Type3 :
    277   String.string -> (Identifiers.universe -> 'a1 -> ('a2,
     270  PreIdentifiers.identifierTag -> (Identifiers.universe -> 'a1 -> ('a2,
    278271  Identifiers.universe) Types.prod) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __
    279272  -> __ -> 'a3) -> 'a3
    280273
    281274val related_globals_gen_rect_Type2 :
    282   String.string -> (Identifiers.universe -> 'a1 -> ('a2,
     275  PreIdentifiers.identifierTag -> (Identifiers.universe -> 'a1 -> ('a2,
    283276  Identifiers.universe) Types.prod) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __
    284277  -> __ -> 'a3) -> 'a3
    285278
    286279val related_globals_gen_rect_Type1 :
    287   String.string -> (Identifiers.universe -> 'a1 -> ('a2,
     280  PreIdentifiers.identifierTag -> (Identifiers.universe -> 'a1 -> ('a2,
    288281  Identifiers.universe) Types.prod) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __
    289282  -> __ -> 'a3) -> 'a3
    290283
    291284val related_globals_gen_rect_Type0 :
    292   String.string -> (Identifiers.universe -> 'a1 -> ('a2,
     285  PreIdentifiers.identifierTag -> (Identifiers.universe -> 'a1 -> ('a2,
    293286  Identifiers.universe) Types.prod) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __
    294287  -> __ -> 'a3) -> 'a3
    295288
    296289val related_globals_gen_inv_rect_Type4 :
    297   String.string -> (Identifiers.universe -> 'a1 -> ('a2,
     290  PreIdentifiers.identifierTag -> (Identifiers.universe -> 'a1 -> ('a2,
    298291  Identifiers.universe) Types.prod) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __
    299292  -> __ -> __ -> 'a3) -> 'a3
    300293
    301294val related_globals_gen_inv_rect_Type3 :
    302   String.string -> (Identifiers.universe -> 'a1 -> ('a2,
     295  PreIdentifiers.identifierTag -> (Identifiers.universe -> 'a1 -> ('a2,
    303296  Identifiers.universe) Types.prod) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __
    304297  -> __ -> __ -> 'a3) -> 'a3
    305298
    306299val related_globals_gen_inv_rect_Type2 :
    307   String.string -> (Identifiers.universe -> 'a1 -> ('a2,
     300  PreIdentifiers.identifierTag -> (Identifiers.universe -> 'a1 -> ('a2,
    308301  Identifiers.universe) Types.prod) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __
    309302  -> __ -> __ -> 'a3) -> 'a3
    310303
    311304val related_globals_gen_inv_rect_Type1 :
    312   String.string -> (Identifiers.universe -> 'a1 -> ('a2,
     305  PreIdentifiers.identifierTag -> (Identifiers.universe -> 'a1 -> ('a2,
    313306  Identifiers.universe) Types.prod) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __
    314307  -> __ -> __ -> 'a3) -> 'a3
    315308
    316309val related_globals_gen_inv_rect_Type0 :
    317   String.string -> (Identifiers.universe -> 'a1 -> ('a2,
     310  PreIdentifiers.identifierTag -> (Identifiers.universe -> 'a1 -> ('a2,
    318311  Identifiers.universe) Types.prod) -> 'a1 genv_t -> 'a2 genv_t -> (__ -> __
    319312  -> __ -> __ -> 'a3) -> 'a3
    320313
    321314val related_globals_gen_discr :
    322   String.string -> (Identifiers.universe -> 'a1 -> ('a2,
     315  PreIdentifiers.identifierTag -> (Identifiers.universe -> 'a1 -> ('a2,
    323316  Identifiers.universe) Types.prod) -> 'a1 genv_t -> 'a2 genv_t -> __
    324317
    325318val related_globals_gen_jmdiscr :
    326   String.string -> (Identifiers.universe -> 'a1 -> ('a2,
     319  PreIdentifiers.identifierTag -> (Identifiers.universe -> 'a1 -> ('a2,
    327320  Identifiers.universe) Types.prod) -> 'a1 genv_t -> 'a2 genv_t -> __
    328321
Note: See TracChangeset for help on using the changeset viewer.