Changeset 2730 for extracted/globalenvs.mli
 Timestamp:
 Feb 25, 2013, 9:54:49 PM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

extracted/globalenvs.mli
r2717 r2730 209 209 val symbol_of_function_block : 'a1 genv_t > Pointers.block > AST.ident 210 210 211 val symbol_of_function_block' : 212 'a1 genv_t > Pointers.block > 'a1 > AST.ident 213 214 val find_funct_ptr_id : 215 'a1 genv_t > Pointers.block > ('a1, AST.ident) Types.prod Types.option 216 217 val symbol_of_function_val : 'a1 genv_t > Values.val0 > AST.ident 218 219 val symbol_of_function_val' : 'a1 genv_t > Values.val0 > 'a1 > AST.ident 220 221 val find_funct_id : 222 'a1 genv_t > Values.val0 > ('a1, AST.ident) Types.prod Types.option 223 211 224 val nat_plus_pos : Nat.nat > Positive.pos > Positive.pos 212 225 … … 218 231 219 232 val related_globals_rect_Type4 : 220 ('a1 > 'a2) > 'a1 genv_t > 'a2 genv_t > (__ > __ > __ > 'a3) > 'a3 233 ('a1 > 'a2) > 'a1 genv_t > 'a2 genv_t > (__ > __ > __ > __ > 'a3) 234 > 'a3 221 235 222 236 val related_globals_rect_Type5 : 223 ('a1 > 'a2) > 'a1 genv_t > 'a2 genv_t > (__ > __ > __ > 'a3) > 'a3 237 ('a1 > 'a2) > 'a1 genv_t > 'a2 genv_t > (__ > __ > __ > __ > 'a3) 238 > 'a3 224 239 225 240 val related_globals_rect_Type3 : 226 ('a1 > 'a2) > 'a1 genv_t > 'a2 genv_t > (__ > __ > __ > 'a3) > 'a3 241 ('a1 > 'a2) > 'a1 genv_t > 'a2 genv_t > (__ > __ > __ > __ > 'a3) 242 > 'a3 227 243 228 244 val related_globals_rect_Type2 : 229 ('a1 > 'a2) > 'a1 genv_t > 'a2 genv_t > (__ > __ > __ > 'a3) > 'a3 245 ('a1 > 'a2) > 'a1 genv_t > 'a2 genv_t > (__ > __ > __ > __ > 'a3) 246 > 'a3 230 247 231 248 val related_globals_rect_Type1 : 232 ('a1 > 'a2) > 'a1 genv_t > 'a2 genv_t > (__ > __ > __ > 'a3) > 'a3 249 ('a1 > 'a2) > 'a1 genv_t > 'a2 genv_t > (__ > __ > __ > __ > 'a3) 250 > 'a3 233 251 234 252 val related_globals_rect_Type0 : 235 ('a1 > 'a2) > 'a1 genv_t > 'a2 genv_t > (__ > __ > __ > 'a3) > 'a3 253 ('a1 > 'a2) > 'a1 genv_t > 'a2 genv_t > (__ > __ > __ > __ > 'a3) 254 > 'a3 236 255 237 256 val related_globals_inv_rect_Type4 : 238 ('a1 > 'a2) > 'a1 genv_t > 'a2 genv_t > (__ > __ > __ > __ > 'a3)239 > 'a3257 ('a1 > 'a2) > 'a1 genv_t > 'a2 genv_t > (__ > __ > __ > __ > __ > 258 'a3) > 'a3 240 259 241 260 val related_globals_inv_rect_Type3 : 242 ('a1 > 'a2) > 'a1 genv_t > 'a2 genv_t > (__ > __ > __ > __ > 'a3)243 > 'a3261 ('a1 > 'a2) > 'a1 genv_t > 'a2 genv_t > (__ > __ > __ > __ > __ > 262 'a3) > 'a3 244 263 245 264 val related_globals_inv_rect_Type2 : 246 ('a1 > 'a2) > 'a1 genv_t > 'a2 genv_t > (__ > __ > __ > __ > 'a3)247 > 'a3265 ('a1 > 'a2) > 'a1 genv_t > 'a2 genv_t > (__ > __ > __ > __ > __ > 266 'a3) > 'a3 248 267 249 268 val related_globals_inv_rect_Type1 : 250 ('a1 > 'a2) > 'a1 genv_t > 'a2 genv_t > (__ > __ > __ > __ > 'a3)251 > 'a3269 ('a1 > 'a2) > 'a1 genv_t > 'a2 genv_t > (__ > __ > __ > __ > __ > 270 'a3) > 'a3 252 271 253 272 val related_globals_inv_rect_Type0 : 254 ('a1 > 'a2) > 'a1 genv_t > 'a2 genv_t > (__ > __ > __ > __ > 'a3)255 > 'a3273 ('a1 > 'a2) > 'a1 genv_t > 'a2 genv_t > (__ > __ > __ > __ > __ > 274 'a3) > 'a3 256 275 257 276 val related_globals_discr : ('a1 > 'a2) > 'a1 genv_t > 'a2 genv_t > __ … … 262 281 PreIdentifiers.identifierTag > (Identifiers.universe > 'a1 > ('a2, 263 282 Identifiers.universe) Types.prod) > 'a1 genv_t > 'a2 genv_t > (__ > __ 264 > __ > 'a3) > 'a3283 > __ > __ > 'a3) > 'a3 265 284 266 285 val related_globals_gen_rect_Type5 : 267 286 PreIdentifiers.identifierTag > (Identifiers.universe > 'a1 > ('a2, 268 287 Identifiers.universe) Types.prod) > 'a1 genv_t > 'a2 genv_t > (__ > __ 269 > __ > 'a3) > 'a3288 > __ > __ > 'a3) > 'a3 270 289 271 290 val related_globals_gen_rect_Type3 : 272 291 PreIdentifiers.identifierTag > (Identifiers.universe > 'a1 > ('a2, 273 292 Identifiers.universe) Types.prod) > 'a1 genv_t > 'a2 genv_t > (__ > __ 274 > __ > 'a3) > 'a3293 > __ > __ > 'a3) > 'a3 275 294 276 295 val related_globals_gen_rect_Type2 : 277 296 PreIdentifiers.identifierTag > (Identifiers.universe > 'a1 > ('a2, 278 297 Identifiers.universe) Types.prod) > 'a1 genv_t > 'a2 genv_t > (__ > __ 279 > __ > 'a3) > 'a3298 > __ > __ > 'a3) > 'a3 280 299 281 300 val related_globals_gen_rect_Type1 : 282 301 PreIdentifiers.identifierTag > (Identifiers.universe > 'a1 > ('a2, 283 302 Identifiers.universe) Types.prod) > 'a1 genv_t > 'a2 genv_t > (__ > __ 284 > __ > 'a3) > 'a3303 > __ > __ > 'a3) > 'a3 285 304 286 305 val related_globals_gen_rect_Type0 : 287 306 PreIdentifiers.identifierTag > (Identifiers.universe > 'a1 > ('a2, 288 307 Identifiers.universe) Types.prod) > 'a1 genv_t > 'a2 genv_t > (__ > __ 289 > __ > 'a3) > 'a3308 > __ > __ > 'a3) > 'a3 290 309 291 310 val related_globals_gen_inv_rect_Type4 : 292 311 PreIdentifiers.identifierTag > (Identifiers.universe > 'a1 > ('a2, 293 312 Identifiers.universe) Types.prod) > 'a1 genv_t > 'a2 genv_t > (__ > __ 294 > __ > __ > 'a3) > 'a3313 > __ > __ > __ > 'a3) > 'a3 295 314 296 315 val related_globals_gen_inv_rect_Type3 : 297 316 PreIdentifiers.identifierTag > (Identifiers.universe > 'a1 > ('a2, 298 317 Identifiers.universe) Types.prod) > 'a1 genv_t > 'a2 genv_t > (__ > __ 299 > __ > __ > 'a3) > 'a3318 > __ > __ > __ > 'a3) > 'a3 300 319 301 320 val related_globals_gen_inv_rect_Type2 : 302 321 PreIdentifiers.identifierTag > (Identifiers.universe > 'a1 > ('a2, 303 322 Identifiers.universe) Types.prod) > 'a1 genv_t > 'a2 genv_t > (__ > __ 304 > __ > __ > 'a3) > 'a3323 > __ > __ > __ > 'a3) > 'a3 305 324 306 325 val related_globals_gen_inv_rect_Type1 : 307 326 PreIdentifiers.identifierTag > (Identifiers.universe > 'a1 > ('a2, 308 327 Identifiers.universe) Types.prod) > 'a1 genv_t > 'a2 genv_t > (__ > __ 309 > __ > __ > 'a3) > 'a3328 > __ > __ > __ > 'a3) > 'a3 310 329 311 330 val related_globals_gen_inv_rect_Type0 : 312 331 PreIdentifiers.identifierTag > (Identifiers.universe > 'a1 > ('a2, 313 332 Identifiers.universe) Types.prod) > 'a1 genv_t > 'a2 genv_t > (__ > __ 314 > __ > __ > 'a3) > 'a3333 > __ > __ > __ > 'a3) > 'a3 315 334 316 335 val related_globals_gen_discr :
Note: See TracChangeset
for help on using the changeset viewer.