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

...

File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/pointers.mli

    r2601 r2649  
    55open Arithmetic
    66
    7 open Char
    8 
    9 open String
    10 
    117open Extranat
    128
     
    5551open Deqsets
    5652
     53open ErrorMessages
     54
    5755open PreIdentifiers
    5856
     
    7169open Identifiers
    7270
    73 open Coqlib
    74 
    75 open Floats
    76 
    7771open Integers
    7872
    7973open AST
    8074
    81 type block = { block_region : AST.region; block_id : Z.z }
    82 
    83 val block_rect_Type4 : (AST.region -> Z.z -> 'a1) -> block -> 'a1
    84 
    85 val block_rect_Type5 : (AST.region -> Z.z -> 'a1) -> block -> 'a1
    86 
    87 val block_rect_Type3 : (AST.region -> Z.z -> 'a1) -> block -> 'a1
    88 
    89 val block_rect_Type2 : (AST.region -> Z.z -> 'a1) -> block -> 'a1
    90 
    91 val block_rect_Type1 : (AST.region -> Z.z -> 'a1) -> block -> 'a1
    92 
    93 val block_rect_Type0 : (AST.region -> Z.z -> 'a1) -> block -> 'a1
     75type block =
     76  Z.z
     77  (* singleton inductive, whose constructor was mk_block *)
     78
     79val block_rect_Type4 : (Z.z -> 'a1) -> block -> 'a1
     80
     81val block_rect_Type5 : (Z.z -> 'a1) -> block -> 'a1
     82
     83val block_rect_Type3 : (Z.z -> 'a1) -> block -> 'a1
     84
     85val block_rect_Type2 : (Z.z -> 'a1) -> block -> 'a1
     86
     87val block_rect_Type1 : (Z.z -> 'a1) -> block -> 'a1
     88
     89val block_rect_Type0 : (Z.z -> 'a1) -> block -> 'a1
     90
     91val block_id : block -> Z.z
     92
     93val block_inv_rect_Type4 : block -> (Z.z -> __ -> 'a1) -> 'a1
     94
     95val block_inv_rect_Type3 : block -> (Z.z -> __ -> 'a1) -> 'a1
     96
     97val block_inv_rect_Type2 : block -> (Z.z -> __ -> 'a1) -> 'a1
     98
     99val block_inv_rect_Type1 : block -> (Z.z -> __ -> 'a1) -> 'a1
     100
     101val block_inv_rect_Type0 : block -> (Z.z -> __ -> 'a1) -> 'a1
     102
     103val block_discr : block -> block -> __
     104
     105val block_jmdiscr : block -> block -> __
    94106
    95107val block_region : block -> AST.region
    96108
    97 val block_id : block -> Z.z
    98 
    99 val block_inv_rect_Type4 : block -> (AST.region -> Z.z -> __ -> 'a1) -> 'a1
    100 
    101 val block_inv_rect_Type3 : block -> (AST.region -> Z.z -> __ -> 'a1) -> 'a1
    102 
    103 val block_inv_rect_Type2 : block -> (AST.region -> Z.z -> __ -> 'a1) -> 'a1
    104 
    105 val block_inv_rect_Type1 : block -> (AST.region -> Z.z -> __ -> 'a1) -> 'a1
    106 
    107 val block_inv_rect_Type0 : block -> (AST.region -> Z.z -> __ -> 'a1) -> 'a1
    108 
    109 val block_discr : block -> block -> __
    110 
    111 val block_jmdiscr : block -> block -> __
     109val dummy_block_code : block
    112110
    113111val eq_block : block -> block -> Bool.bool
Note: See TracChangeset for help on using the changeset viewer.