Changeset 2743 for extracted/pointers.ml


Ignore:
Timestamp:
Feb 27, 2013, 9:27:58 PM (8 years ago)
Author:
sacerdot
Message:

Latest version of the compiler, extracted with the latest version of Matita.
Some files still need some manual patching to avoid an extraction bug
(see PROBLEMS file).

File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/pointers.ml

    r2730 r2743  
    8080
    8181(** val block_rect_Type4 : (Z.z -> 'a1) -> block -> 'a1 **)
    82 let rec block_rect_Type4 h_mk_block x_5622 =
    83   let block_id = x_5622 in h_mk_block block_id
     82let rec block_rect_Type4 h_mk_block x_4976 =
     83  let block_id = x_4976 in h_mk_block block_id
    8484
    8585(** val block_rect_Type5 : (Z.z -> 'a1) -> block -> 'a1 **)
    86 let rec block_rect_Type5 h_mk_block x_5624 =
    87   let block_id = x_5624 in h_mk_block block_id
     86let rec block_rect_Type5 h_mk_block x_4978 =
     87  let block_id = x_4978 in h_mk_block block_id
    8888
    8989(** val block_rect_Type3 : (Z.z -> 'a1) -> block -> 'a1 **)
    90 let rec block_rect_Type3 h_mk_block x_5626 =
    91   let block_id = x_5626 in h_mk_block block_id
     90let rec block_rect_Type3 h_mk_block x_4980 =
     91  let block_id = x_4980 in h_mk_block block_id
    9292
    9393(** val block_rect_Type2 : (Z.z -> 'a1) -> block -> 'a1 **)
    94 let rec block_rect_Type2 h_mk_block x_5628 =
    95   let block_id = x_5628 in h_mk_block block_id
     94let rec block_rect_Type2 h_mk_block x_4982 =
     95  let block_id = x_4982 in h_mk_block block_id
    9696
    9797(** val block_rect_Type1 : (Z.z -> 'a1) -> block -> 'a1 **)
    98 let rec block_rect_Type1 h_mk_block x_5630 =
    99   let block_id = x_5630 in h_mk_block block_id
     98let rec block_rect_Type1 h_mk_block x_4984 =
     99  let block_id = x_4984 in h_mk_block block_id
    100100
    101101(** val block_rect_Type0 : (Z.z -> 'a1) -> block -> 'a1 **)
    102 let rec block_rect_Type0 h_mk_block x_5632 =
    103   let block_id = x_5632 in h_mk_block block_id
     102let rec block_rect_Type0 h_mk_block x_4986 =
     103  let block_id = x_4986 in h_mk_block block_id
    104104
    105105(** val block_id : block -> Z.z **)
     
    163163
    164164(** val offset_rect_Type4 : (BitVector.bitVector -> 'a1) -> offset -> 'a1 **)
    165 let rec offset_rect_Type4 h_mk_offset x_5648 =
    166   let offv = x_5648 in h_mk_offset offv
     165let rec offset_rect_Type4 h_mk_offset x_5002 =
     166  let offv = x_5002 in h_mk_offset offv
    167167
    168168(** val offset_rect_Type5 : (BitVector.bitVector -> 'a1) -> offset -> 'a1 **)
    169 let rec offset_rect_Type5 h_mk_offset x_5650 =
    170   let offv = x_5650 in h_mk_offset offv
     169let rec offset_rect_Type5 h_mk_offset x_5004 =
     170  let offv = x_5004 in h_mk_offset offv
    171171
    172172(** val offset_rect_Type3 : (BitVector.bitVector -> 'a1) -> offset -> 'a1 **)
    173 let rec offset_rect_Type3 h_mk_offset x_5652 =
    174   let offv = x_5652 in h_mk_offset offv
     173let rec offset_rect_Type3 h_mk_offset x_5006 =
     174  let offv = x_5006 in h_mk_offset offv
    175175
    176176(** val offset_rect_Type2 : (BitVector.bitVector -> 'a1) -> offset -> 'a1 **)
    177 let rec offset_rect_Type2 h_mk_offset x_5654 =
    178   let offv = x_5654 in h_mk_offset offv
     177let rec offset_rect_Type2 h_mk_offset x_5008 =
     178  let offv = x_5008 in h_mk_offset offv
    179179
    180180(** val offset_rect_Type1 : (BitVector.bitVector -> 'a1) -> offset -> 'a1 **)
    181 let rec offset_rect_Type1 h_mk_offset x_5656 =
    182   let offv = x_5656 in h_mk_offset offv
     181let rec offset_rect_Type1 h_mk_offset x_5010 =
     182  let offv = x_5010 in h_mk_offset offv
    183183
    184184(** val offset_rect_Type0 : (BitVector.bitVector -> 'a1) -> offset -> 'a1 **)
    185 let rec offset_rect_Type0 h_mk_offset x_5658 =
    186   let offv = x_5658 in h_mk_offset offv
     185let rec offset_rect_Type0 h_mk_offset x_5012 =
     186  let offv = x_5012 in h_mk_offset offv
    187187
    188188(** val offv : offset -> BitVector.bitVector **)
     
    280280
    281281(** val pointer_rect_Type4 : (block -> offset -> 'a1) -> pointer -> 'a1 **)
    282 let rec pointer_rect_Type4 h_mk_pointer x_5674 =
    283   let { pblock = pblock0; poff = poff0 } = x_5674 in
     282let rec pointer_rect_Type4 h_mk_pointer x_5028 =
     283  let { pblock = pblock0; poff = poff0 } = x_5028 in
    284284  h_mk_pointer pblock0 poff0
    285285
    286286(** val pointer_rect_Type5 : (block -> offset -> 'a1) -> pointer -> 'a1 **)
    287 let rec pointer_rect_Type5 h_mk_pointer x_5676 =
    288   let { pblock = pblock0; poff = poff0 } = x_5676 in
     287let rec pointer_rect_Type5 h_mk_pointer x_5030 =
     288  let { pblock = pblock0; poff = poff0 } = x_5030 in
    289289  h_mk_pointer pblock0 poff0
    290290
    291291(** val pointer_rect_Type3 : (block -> offset -> 'a1) -> pointer -> 'a1 **)
    292 let rec pointer_rect_Type3 h_mk_pointer x_5678 =
    293   let { pblock = pblock0; poff = poff0 } = x_5678 in
     292let rec pointer_rect_Type3 h_mk_pointer x_5032 =
     293  let { pblock = pblock0; poff = poff0 } = x_5032 in
    294294  h_mk_pointer pblock0 poff0
    295295
    296296(** val pointer_rect_Type2 : (block -> offset -> 'a1) -> pointer -> 'a1 **)
    297 let rec pointer_rect_Type2 h_mk_pointer x_5680 =
    298   let { pblock = pblock0; poff = poff0 } = x_5680 in
     297let rec pointer_rect_Type2 h_mk_pointer x_5034 =
     298  let { pblock = pblock0; poff = poff0 } = x_5034 in
    299299  h_mk_pointer pblock0 poff0
    300300
    301301(** val pointer_rect_Type1 : (block -> offset -> 'a1) -> pointer -> 'a1 **)
    302 let rec pointer_rect_Type1 h_mk_pointer x_5682 =
    303   let { pblock = pblock0; poff = poff0 } = x_5682 in
     302let rec pointer_rect_Type1 h_mk_pointer x_5036 =
     303  let { pblock = pblock0; poff = poff0 } = x_5036 in
    304304  h_mk_pointer pblock0 poff0
    305305
    306306(** val pointer_rect_Type0 : (block -> offset -> 'a1) -> pointer -> 'a1 **)
    307 let rec pointer_rect_Type0 h_mk_pointer x_5684 =
    308   let { pblock = pblock0; poff = poff0 } = x_5684 in
     307let rec pointer_rect_Type0 h_mk_pointer x_5038 =
     308  let { pblock = pblock0; poff = poff0 } = x_5038 in
    309309  h_mk_pointer pblock0 poff0
    310310
Note: See TracChangeset for help on using the changeset viewer.