Changeset 2649 for extracted/globalenvs.mli
 Timestamp:
 Feb 7, 2013, 10:43:49 PM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

extracted/globalenvs.mli
r2601 r2649 1 1 open Preamble 2 2 3 open ErrorMessages 4 3 5 open Option 4 6 … … 13 15 open Positive 14 16 15 open Char16 17 open String18 19 17 open PreIdentifiers 20 18 … … 51 49 open Identifiers 52 50 51 open Arithmetic 52 53 open Vector 54 55 open Div_and_mod 56 57 open Util 58 59 open FoldStuff 60 61 open BitVector 62 63 open Extranat 64 65 open Integers 66 67 open AST 68 53 69 open Coqlib 54 55 open Floats56 57 open Arithmetic58 59 open Vector60 61 open Div_and_mod62 63 open Util64 65 open FoldStuff66 67 open BitVector68 69 open Extranat70 71 open Integers72 73 open AST74 70 75 71 open Values … … 177 173 178 174 val size_init_data_list : AST.init_data List.list > Nat.nat 179 180 val initDataStoreFailed : String.string181 175 182 176 val add_globals : … … 216 210 217 211 val 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 221 214 222 215 val prod_jmdiscr0 : ('a1, 'a2) Types.prod > ('a1, 'a2) Types.prod > __ … … 265 258 266 259 val related_globals_gen_rect_Type4 : 267 String.string > (Identifiers.universe > 'a1 > ('a2,260 PreIdentifiers.identifierTag > (Identifiers.universe > 'a1 > ('a2, 268 261 Identifiers.universe) Types.prod) > 'a1 genv_t > 'a2 genv_t > (__ > __ 269 262 > __ > 'a3) > 'a3 270 263 271 264 val related_globals_gen_rect_Type5 : 272 String.string > (Identifiers.universe > 'a1 > ('a2,265 PreIdentifiers.identifierTag > (Identifiers.universe > 'a1 > ('a2, 273 266 Identifiers.universe) Types.prod) > 'a1 genv_t > 'a2 genv_t > (__ > __ 274 267 > __ > 'a3) > 'a3 275 268 276 269 val related_globals_gen_rect_Type3 : 277 String.string > (Identifiers.universe > 'a1 > ('a2,270 PreIdentifiers.identifierTag > (Identifiers.universe > 'a1 > ('a2, 278 271 Identifiers.universe) Types.prod) > 'a1 genv_t > 'a2 genv_t > (__ > __ 279 272 > __ > 'a3) > 'a3 280 273 281 274 val related_globals_gen_rect_Type2 : 282 String.string > (Identifiers.universe > 'a1 > ('a2,275 PreIdentifiers.identifierTag > (Identifiers.universe > 'a1 > ('a2, 283 276 Identifiers.universe) Types.prod) > 'a1 genv_t > 'a2 genv_t > (__ > __ 284 277 > __ > 'a3) > 'a3 285 278 286 279 val related_globals_gen_rect_Type1 : 287 String.string > (Identifiers.universe > 'a1 > ('a2,280 PreIdentifiers.identifierTag > (Identifiers.universe > 'a1 > ('a2, 288 281 Identifiers.universe) Types.prod) > 'a1 genv_t > 'a2 genv_t > (__ > __ 289 282 > __ > 'a3) > 'a3 290 283 291 284 val related_globals_gen_rect_Type0 : 292 String.string > (Identifiers.universe > 'a1 > ('a2,285 PreIdentifiers.identifierTag > (Identifiers.universe > 'a1 > ('a2, 293 286 Identifiers.universe) Types.prod) > 'a1 genv_t > 'a2 genv_t > (__ > __ 294 287 > __ > 'a3) > 'a3 295 288 296 289 val related_globals_gen_inv_rect_Type4 : 297 String.string > (Identifiers.universe > 'a1 > ('a2,290 PreIdentifiers.identifierTag > (Identifiers.universe > 'a1 > ('a2, 298 291 Identifiers.universe) Types.prod) > 'a1 genv_t > 'a2 genv_t > (__ > __ 299 292 > __ > __ > 'a3) > 'a3 300 293 301 294 val related_globals_gen_inv_rect_Type3 : 302 String.string > (Identifiers.universe > 'a1 > ('a2,295 PreIdentifiers.identifierTag > (Identifiers.universe > 'a1 > ('a2, 303 296 Identifiers.universe) Types.prod) > 'a1 genv_t > 'a2 genv_t > (__ > __ 304 297 > __ > __ > 'a3) > 'a3 305 298 306 299 val related_globals_gen_inv_rect_Type2 : 307 String.string > (Identifiers.universe > 'a1 > ('a2,300 PreIdentifiers.identifierTag > (Identifiers.universe > 'a1 > ('a2, 308 301 Identifiers.universe) Types.prod) > 'a1 genv_t > 'a2 genv_t > (__ > __ 309 302 > __ > __ > 'a3) > 'a3 310 303 311 304 val related_globals_gen_inv_rect_Type1 : 312 String.string > (Identifiers.universe > 'a1 > ('a2,305 PreIdentifiers.identifierTag > (Identifiers.universe > 'a1 > ('a2, 313 306 Identifiers.universe) Types.prod) > 'a1 genv_t > 'a2 genv_t > (__ > __ 314 307 > __ > __ > 'a3) > 'a3 315 308 316 309 val related_globals_gen_inv_rect_Type0 : 317 String.string > (Identifiers.universe > 'a1 > ('a2,310 PreIdentifiers.identifierTag > (Identifiers.universe > 'a1 > ('a2, 318 311 Identifiers.universe) Types.prod) > 'a1 genv_t > 'a2 genv_t > (__ > __ 319 312 > __ > __ > 'a3) > 'a3 320 313 321 314 val related_globals_gen_discr : 322 String.string > (Identifiers.universe > 'a1 > ('a2,315 PreIdentifiers.identifierTag > (Identifiers.universe > 'a1 > ('a2, 323 316 Identifiers.universe) Types.prod) > 'a1 genv_t > 'a2 genv_t > __ 324 317 325 318 val related_globals_gen_jmdiscr : 326 String.string > (Identifiers.universe > 'a1 > ('a2,319 PreIdentifiers.identifierTag > (Identifiers.universe > 'a1 > ('a2, 327 320 Identifiers.universe) Types.prod) > 'a1 genv_t > 'a2 genv_t > __ 328 321
Note: See TracChangeset
for help on using the changeset viewer.