Ignore:
Timestamp:
Feb 27, 2013, 9:27:58 PM (7 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/byteValues.ml

    r2730 r2743  
    8989    (Pointers.block Types.sig0 -> Positive.pos -> 'a1) -> program_counter ->
    9090    'a1 **)
    91 let rec program_counter_rect_Type4 h_mk_program_counter x_5700 =
    92   let { pc_block = pc_block0; pc_offset = pc_offset0 } = x_5700 in
     91let rec program_counter_rect_Type4 h_mk_program_counter x_6100 =
     92  let { pc_block = pc_block0; pc_offset = pc_offset0 } = x_6100 in
    9393  h_mk_program_counter pc_block0 pc_offset0
    9494
     
    9696    (Pointers.block Types.sig0 -> Positive.pos -> 'a1) -> program_counter ->
    9797    'a1 **)
    98 let rec program_counter_rect_Type5 h_mk_program_counter x_5702 =
    99   let { pc_block = pc_block0; pc_offset = pc_offset0 } = x_5702 in
     98let rec program_counter_rect_Type5 h_mk_program_counter x_6102 =
     99  let { pc_block = pc_block0; pc_offset = pc_offset0 } = x_6102 in
    100100  h_mk_program_counter pc_block0 pc_offset0
    101101
     
    103103    (Pointers.block Types.sig0 -> Positive.pos -> 'a1) -> program_counter ->
    104104    'a1 **)
    105 let rec program_counter_rect_Type3 h_mk_program_counter x_5704 =
    106   let { pc_block = pc_block0; pc_offset = pc_offset0 } = x_5704 in
     105let rec program_counter_rect_Type3 h_mk_program_counter x_6104 =
     106  let { pc_block = pc_block0; pc_offset = pc_offset0 } = x_6104 in
    107107  h_mk_program_counter pc_block0 pc_offset0
    108108
     
    110110    (Pointers.block Types.sig0 -> Positive.pos -> 'a1) -> program_counter ->
    111111    'a1 **)
    112 let rec program_counter_rect_Type2 h_mk_program_counter x_5706 =
    113   let { pc_block = pc_block0; pc_offset = pc_offset0 } = x_5706 in
     112let rec program_counter_rect_Type2 h_mk_program_counter x_6106 =
     113  let { pc_block = pc_block0; pc_offset = pc_offset0 } = x_6106 in
    114114  h_mk_program_counter pc_block0 pc_offset0
    115115
     
    117117    (Pointers.block Types.sig0 -> Positive.pos -> 'a1) -> program_counter ->
    118118    'a1 **)
    119 let rec program_counter_rect_Type1 h_mk_program_counter x_5708 =
    120   let { pc_block = pc_block0; pc_offset = pc_offset0 } = x_5708 in
     119let rec program_counter_rect_Type1 h_mk_program_counter x_6108 =
     120  let { pc_block = pc_block0; pc_offset = pc_offset0 } = x_6108 in
    121121  h_mk_program_counter pc_block0 pc_offset0
    122122
     
    124124    (Pointers.block Types.sig0 -> Positive.pos -> 'a1) -> program_counter ->
    125125    'a1 **)
    126 let rec program_counter_rect_Type0 h_mk_program_counter x_5710 =
    127   let { pc_block = pc_block0; pc_offset = pc_offset0 } = x_5710 in
     126let rec program_counter_rect_Type0 h_mk_program_counter x_6110 =
     127  let { pc_block = pc_block0; pc_offset = pc_offset0 } = x_6110 in
    128128  h_mk_program_counter pc_block0 pc_offset0
    129129
     
    215215
    216216(** val part_rect_Type4 : (Nat.nat -> __ -> 'a1) -> part -> 'a1 **)
    217 let rec part_rect_Type4 h_mk_part x_5726 =
    218   let part_no = x_5726 in h_mk_part part_no __
     217let rec part_rect_Type4 h_mk_part x_6126 =
     218  let part_no = x_6126 in h_mk_part part_no __
    219219
    220220(** val part_rect_Type5 : (Nat.nat -> __ -> 'a1) -> part -> 'a1 **)
    221 let rec part_rect_Type5 h_mk_part x_5728 =
    222   let part_no = x_5728 in h_mk_part part_no __
     221let rec part_rect_Type5 h_mk_part x_6128 =
     222  let part_no = x_6128 in h_mk_part part_no __
    223223
    224224(** val part_rect_Type3 : (Nat.nat -> __ -> 'a1) -> part -> 'a1 **)
    225 let rec part_rect_Type3 h_mk_part x_5730 =
    226   let part_no = x_5730 in h_mk_part part_no __
     225let rec part_rect_Type3 h_mk_part x_6130 =
     226  let part_no = x_6130 in h_mk_part part_no __
    227227
    228228(** val part_rect_Type2 : (Nat.nat -> __ -> 'a1) -> part -> 'a1 **)
    229 let rec part_rect_Type2 h_mk_part x_5732 =
    230   let part_no = x_5732 in h_mk_part part_no __
     229let rec part_rect_Type2 h_mk_part x_6132 =
     230  let part_no = x_6132 in h_mk_part part_no __
    231231
    232232(** val part_rect_Type1 : (Nat.nat -> __ -> 'a1) -> part -> 'a1 **)
    233 let rec part_rect_Type1 h_mk_part x_5734 =
    234   let part_no = x_5734 in h_mk_part part_no __
     233let rec part_rect_Type1 h_mk_part x_6134 =
     234  let part_no = x_6134 in h_mk_part part_no __
    235235
    236236(** val part_rect_Type0 : (Nat.nat -> __ -> 'a1) -> part -> 'a1 **)
    237 let rec part_rect_Type0 h_mk_part x_5736 =
    238   let part_no = x_5736 in h_mk_part part_no __
     237let rec part_rect_Type0 h_mk_part x_6136 =
     238  let part_no = x_6136 in h_mk_part part_no __
    239239
    240240(** val part_no : part -> Nat.nat **)
     
    307307let part_from_sig n_sig =
    308308  Types.pi1 n_sig
     309
     310(** val dpi1__o__part_no__o__inject__o__sig_to_part__o__inject :
     311    (part, 'a1) Types.dPair -> part Types.sig0 **)
     312let dpi1__o__part_no__o__inject__o__sig_to_part__o__inject x2 =
     313  part_from_sig (dpi1__o__part_no__o__inject x2)
     314
     315(** val dpi1__o__part_no__o__inject__o__sig_to_part__o__part_no__o__inject :
     316    (part, 'a1) Types.dPair -> Nat.nat Types.sig0 **)
     317let dpi1__o__part_no__o__inject__o__sig_to_part__o__part_no__o__inject x2 =
     318  part_no__o__inject (part_from_sig (dpi1__o__part_no__o__inject x2))
     319
     320(** val dpi1__o__part_no__o__inject__o__sig_to_part__o__part_no__o__Z_of_nat :
     321    (part, 'a1) Types.dPair -> Z.z **)
     322let dpi1__o__part_no__o__inject__o__sig_to_part__o__part_no__o__Z_of_nat x1 =
     323  part_no__o__Z_of_nat (part_from_sig (dpi1__o__part_no__o__inject x1))
     324
     325(** val dpi1__o__part_no__o__inject__o__sig_to_part__o__part_no :
     326    (part, 'a1) Types.dPair -> Nat.nat **)
     327let dpi1__o__part_no__o__inject__o__sig_to_part__o__part_no x1 =
     328  part_no (part_from_sig (dpi1__o__part_no__o__inject x1))
     329
     330(** val eject__o__part_no__o__inject__o__sig_to_part__o__inject :
     331    part Types.sig0 -> part Types.sig0 **)
     332let eject__o__part_no__o__inject__o__sig_to_part__o__inject x2 =
     333  part_from_sig (eject__o__part_no__o__inject x2)
     334
     335(** val eject__o__part_no__o__inject__o__sig_to_part__o__part_no__o__inject :
     336    part Types.sig0 -> Nat.nat Types.sig0 **)
     337let eject__o__part_no__o__inject__o__sig_to_part__o__part_no__o__inject x2 =
     338  part_no__o__inject (part_from_sig (eject__o__part_no__o__inject x2))
     339
     340(** val eject__o__part_no__o__inject__o__sig_to_part__o__part_no__o__Z_of_nat :
     341    part Types.sig0 -> Z.z **)
     342let eject__o__part_no__o__inject__o__sig_to_part__o__part_no__o__Z_of_nat x1 =
     343  part_no__o__Z_of_nat (part_from_sig (eject__o__part_no__o__inject x1))
     344
     345(** val eject__o__part_no__o__inject__o__sig_to_part__o__part_no :
     346    part Types.sig0 -> Nat.nat **)
     347let eject__o__part_no__o__inject__o__sig_to_part__o__part_no x1 =
     348  part_no (part_from_sig (eject__o__part_no__o__inject x1))
     349
     350(** val inject__o__sig_to_part__o__inject : Nat.nat -> part Types.sig0 **)
     351let inject__o__sig_to_part__o__inject x0 =
     352  part_from_sig x0
     353
     354(** val inject__o__sig_to_part__o__part_no__o__inject :
     355    Nat.nat -> Nat.nat Types.sig0 **)
     356let inject__o__sig_to_part__o__part_no__o__inject x0 =
     357  part_no__o__inject (part_from_sig x0)
     358
     359(** val inject__o__sig_to_part__o__part_no__o__Z_of_nat : Nat.nat -> Z.z **)
     360let inject__o__sig_to_part__o__part_no__o__Z_of_nat x0 =
     361  part_no__o__Z_of_nat (part_from_sig x0)
     362
     363(** val inject__o__sig_to_part__o__part_no : Nat.nat -> Nat.nat **)
     364let inject__o__sig_to_part__o__part_no x0 =
     365  part_no (part_from_sig x0)
     366
     367(** val part_no__o__inject__o__sig_to_part__o__inject :
     368    part -> part Types.sig0 **)
     369let part_no__o__inject__o__sig_to_part__o__inject x0 =
     370  part_from_sig (part_no__o__inject x0)
     371
     372(** val part_no__o__inject__o__sig_to_part__o__part_no__o__inject :
     373    part -> Nat.nat Types.sig0 **)
     374let part_no__o__inject__o__sig_to_part__o__part_no__o__inject x0 =
     375  part_no__o__inject (part_from_sig (part_no__o__inject x0))
     376
     377(** val part_no__o__inject__o__sig_to_part__o__part_no__o__Z_of_nat :
     378    part -> Z.z **)
     379let part_no__o__inject__o__sig_to_part__o__part_no__o__Z_of_nat x0 =
     380  part_no__o__Z_of_nat (part_from_sig (part_no__o__inject x0))
     381
     382(** val part_no__o__inject__o__sig_to_part__o__part_no : part -> Nat.nat **)
     383let part_no__o__inject__o__sig_to_part__o__part_no x0 =
     384  part_no (part_from_sig (part_no__o__inject x0))
     385
     386(** val dpi1__o__sig_to_part__o__inject :
     387    (Nat.nat Types.sig0, 'a1) Types.dPair -> part Types.sig0 **)
     388let dpi1__o__sig_to_part__o__inject x2 =
     389  part_from_sig x2.Types.dpi1
     390
     391(** val dpi1__o__sig_to_part__o__part_no__o__inject :
     392    (Nat.nat Types.sig0, 'a1) Types.dPair -> Nat.nat Types.sig0 **)
     393let dpi1__o__sig_to_part__o__part_no__o__inject x2 =
     394  part_no__o__inject (part_from_sig x2.Types.dpi1)
     395
     396(** val dpi1__o__sig_to_part__o__part_no__o__Z_of_nat :
     397    (Nat.nat Types.sig0, 'a1) Types.dPair -> Z.z **)
     398let dpi1__o__sig_to_part__o__part_no__o__Z_of_nat x1 =
     399  part_no__o__Z_of_nat (part_from_sig x1.Types.dpi1)
     400
     401(** val dpi1__o__sig_to_part__o__part_no :
     402    (Nat.nat Types.sig0, 'a1) Types.dPair -> Nat.nat **)
     403let dpi1__o__sig_to_part__o__part_no x1 =
     404  part_no (part_from_sig x1.Types.dpi1)
     405
     406(** val eject__o__sig_to_part__o__inject :
     407    Nat.nat Types.sig0 Types.sig0 -> part Types.sig0 **)
     408let eject__o__sig_to_part__o__inject x2 =
     409  part_from_sig (Types.pi1 x2)
     410
     411(** val eject__o__sig_to_part__o__part_no__o__inject :
     412    Nat.nat Types.sig0 Types.sig0 -> Nat.nat Types.sig0 **)
     413let eject__o__sig_to_part__o__part_no__o__inject x2 =
     414  part_no__o__inject (part_from_sig (Types.pi1 x2))
     415
     416(** val eject__o__sig_to_part__o__part_no__o__Z_of_nat :
     417    Nat.nat Types.sig0 Types.sig0 -> Z.z **)
     418let eject__o__sig_to_part__o__part_no__o__Z_of_nat x1 =
     419  part_no__o__Z_of_nat (part_from_sig (Types.pi1 x1))
     420
     421(** val eject__o__sig_to_part__o__part_no :
     422    Nat.nat Types.sig0 Types.sig0 -> Nat.nat **)
     423let eject__o__sig_to_part__o__part_no x1 =
     424  part_no (part_from_sig (Types.pi1 x1))
     425
     426(** val sig_to_part__o__part_no : Nat.nat Types.sig0 -> Nat.nat **)
     427let sig_to_part__o__part_no x0 =
     428  part_no (part_from_sig x0)
     429
     430(** val sig_to_part__o__part_no__o__Z_of_nat : Nat.nat Types.sig0 -> Z.z **)
     431let sig_to_part__o__part_no__o__Z_of_nat x0 =
     432  part_no__o__Z_of_nat (part_from_sig x0)
     433
     434(** val sig_to_part__o__part_no__o__inject :
     435    Nat.nat Types.sig0 -> Nat.nat Types.sig0 **)
     436let sig_to_part__o__part_no__o__inject x1 =
     437  part_no__o__inject (part_from_sig x1)
     438
     439(** val sig_to_part__o__inject : Nat.nat Types.sig0 -> part Types.sig0 **)
     440let sig_to_part__o__inject x1 =
     441  part_from_sig x1
     442
     443(** val dpi1__o__part_no__o__inject__o__sig_to_part :
     444    (part, 'a1) Types.dPair -> part **)
     445let dpi1__o__part_no__o__inject__o__sig_to_part x1 =
     446  part_from_sig (dpi1__o__part_no__o__inject x1)
     447
     448(** val eject__o__part_no__o__inject__o__sig_to_part :
     449    part Types.sig0 -> part **)
     450let eject__o__part_no__o__inject__o__sig_to_part x1 =
     451  part_from_sig (eject__o__part_no__o__inject x1)
     452
     453(** val inject__o__sig_to_part : Nat.nat -> part **)
     454let inject__o__sig_to_part x0 =
     455  part_from_sig x0
     456
     457(** val part_no__o__inject__o__sig_to_part : part -> part **)
     458let part_no__o__inject__o__sig_to_part x0 =
     459  part_from_sig (part_no__o__inject x0)
     460
     461(** val dpi1__o__sig_to_part :
     462    (Nat.nat Types.sig0, 'a1) Types.dPair -> part **)
     463let dpi1__o__sig_to_part x1 =
     464  part_from_sig x1.Types.dpi1
     465
     466(** val eject__o__sig_to_part : Nat.nat Types.sig0 Types.sig0 -> part **)
     467let eject__o__sig_to_part x1 =
     468  part_from_sig (Types.pi1 x1)
    309469
    310470type beval =
     
    326486| BVundef -> h_BVundef
    327487| BVnonzero -> h_BVnonzero
    328 | BVXor (x_5770, x_5769, x_5768) -> h_BVXor x_5770 x_5769 x_5768
    329 | BVByte x_5771 -> h_BVByte x_5771
    330 | BVnull x_5772 -> h_BVnull x_5772
    331 | BVptr (x_5774, x_5773) -> h_BVptr x_5774 x_5773
    332 | BVpc (x_5776, x_5775) -> h_BVpc x_5776 x_5775
     488| BVXor (x_6170, x_6169, x_6168) -> h_BVXor x_6170 x_6169 x_6168
     489| BVByte x_6171 -> h_BVByte x_6171
     490| BVnull x_6172 -> h_BVnull x_6172
     491| BVptr (x_6174, x_6173) -> h_BVptr x_6174 x_6173
     492| BVpc (x_6176, x_6175) -> h_BVpc x_6176 x_6175
    333493
    334494(** val beval_rect_Type5 :
     
    340500| BVundef -> h_BVundef
    341501| BVnonzero -> h_BVnonzero
    342 | BVXor (x_5787, x_5786, x_5785) -> h_BVXor x_5787 x_5786 x_5785
    343 | BVByte x_5788 -> h_BVByte x_5788
    344 | BVnull x_5789 -> h_BVnull x_5789
    345 | BVptr (x_5791, x_5790) -> h_BVptr x_5791 x_5790
    346 | BVpc (x_5793, x_5792) -> h_BVpc x_5793 x_5792
     502| BVXor (x_6187, x_6186, x_6185) -> h_BVXor x_6187 x_6186 x_6185
     503| BVByte x_6188 -> h_BVByte x_6188
     504| BVnull x_6189 -> h_BVnull x_6189
     505| BVptr (x_6191, x_6190) -> h_BVptr x_6191 x_6190
     506| BVpc (x_6193, x_6192) -> h_BVpc x_6193 x_6192
    347507
    348508(** val beval_rect_Type3 :
     
    354514| BVundef -> h_BVundef
    355515| BVnonzero -> h_BVnonzero
    356 | BVXor (x_5804, x_5803, x_5802) -> h_BVXor x_5804 x_5803 x_5802
    357 | BVByte x_5805 -> h_BVByte x_5805
    358 | BVnull x_5806 -> h_BVnull x_5806
    359 | BVptr (x_5808, x_5807) -> h_BVptr x_5808 x_5807
    360 | BVpc (x_5810, x_5809) -> h_BVpc x_5810 x_5809
     516| BVXor (x_6204, x_6203, x_6202) -> h_BVXor x_6204 x_6203 x_6202
     517| BVByte x_6205 -> h_BVByte x_6205
     518| BVnull x_6206 -> h_BVnull x_6206
     519| BVptr (x_6208, x_6207) -> h_BVptr x_6208 x_6207
     520| BVpc (x_6210, x_6209) -> h_BVpc x_6210 x_6209
    361521
    362522(** val beval_rect_Type2 :
     
    368528| BVundef -> h_BVundef
    369529| BVnonzero -> h_BVnonzero
    370 | BVXor (x_5821, x_5820, x_5819) -> h_BVXor x_5821 x_5820 x_5819
    371 | BVByte x_5822 -> h_BVByte x_5822
    372 | BVnull x_5823 -> h_BVnull x_5823
    373 | BVptr (x_5825, x_5824) -> h_BVptr x_5825 x_5824
    374 | BVpc (x_5827, x_5826) -> h_BVpc x_5827 x_5826
     530| BVXor (x_6221, x_6220, x_6219) -> h_BVXor x_6221 x_6220 x_6219
     531| BVByte x_6222 -> h_BVByte x_6222
     532| BVnull x_6223 -> h_BVnull x_6223
     533| BVptr (x_6225, x_6224) -> h_BVptr x_6225 x_6224
     534| BVpc (x_6227, x_6226) -> h_BVpc x_6227 x_6226
    375535
    376536(** val beval_rect_Type1 :
     
    382542| BVundef -> h_BVundef
    383543| BVnonzero -> h_BVnonzero
    384 | BVXor (x_5838, x_5837, x_5836) -> h_BVXor x_5838 x_5837 x_5836
    385 | BVByte x_5839 -> h_BVByte x_5839
    386 | BVnull x_5840 -> h_BVnull x_5840
    387 | BVptr (x_5842, x_5841) -> h_BVptr x_5842 x_5841
    388 | BVpc (x_5844, x_5843) -> h_BVpc x_5844 x_5843
     544| BVXor (x_6238, x_6237, x_6236) -> h_BVXor x_6238 x_6237 x_6236
     545| BVByte x_6239 -> h_BVByte x_6239
     546| BVnull x_6240 -> h_BVnull x_6240
     547| BVptr (x_6242, x_6241) -> h_BVptr x_6242 x_6241
     548| BVpc (x_6244, x_6243) -> h_BVpc x_6244 x_6243
    389549
    390550(** val beval_rect_Type0 :
     
    396556| BVundef -> h_BVundef
    397557| BVnonzero -> h_BVnonzero
    398 | BVXor (x_5855, x_5854, x_5853) -> h_BVXor x_5855 x_5854 x_5853
    399 | BVByte x_5856 -> h_BVByte x_5856
    400 | BVnull x_5857 -> h_BVnull x_5857
    401 | BVptr (x_5859, x_5858) -> h_BVptr x_5859 x_5858
    402 | BVpc (x_5861, x_5860) -> h_BVpc x_5861 x_5860
     558| BVXor (x_6255, x_6254, x_6253) -> h_BVXor x_6255 x_6254 x_6253
     559| BVByte x_6256 -> h_BVByte x_6256
     560| BVnull x_6257 -> h_BVnull x_6257
     561| BVptr (x_6259, x_6258) -> h_BVptr x_6259 x_6258
     562| BVpc (x_6261, x_6260) -> h_BVpc x_6261 x_6260
    403563
    404564(** val beval_inv_rect_Type4 :
     
    739899    BitVector.bitVector -> 'a1) -> bebit -> 'a1 **)
    740900let rec bebit_rect_Type4 h_BBbit h_BBundef h_BBptrcarry = function
    741 | BBbit x_5980 -> h_BBbit x_5980
     901| BBbit x_6380 -> h_BBbit x_6380
    742902| BBundef -> h_BBundef
    743 | BBptrcarry (x_5983, x_5982, p, x_5981) ->
    744   h_BBptrcarry x_5983 x_5982 p x_5981
     903| BBptrcarry (x_6383, x_6382, p, x_6381) ->
     904  h_BBptrcarry x_6383 x_6382 p x_6381
    745905
    746906(** val bebit_rect_Type5 :
     
    748908    BitVector.bitVector -> 'a1) -> bebit -> 'a1 **)
    749909let rec bebit_rect_Type5 h_BBbit h_BBundef h_BBptrcarry = function
    750 | BBbit x_5988 -> h_BBbit x_5988
     910| BBbit x_6388 -> h_BBbit x_6388
    751911| BBundef -> h_BBundef
    752 | BBptrcarry (x_5991, x_5990, p, x_5989) ->
    753   h_BBptrcarry x_5991 x_5990 p x_5989
     912| BBptrcarry (x_6391, x_6390, p, x_6389) ->
     913  h_BBptrcarry x_6391 x_6390 p x_6389
    754914
    755915(** val bebit_rect_Type3 :
     
    757917    BitVector.bitVector -> 'a1) -> bebit -> 'a1 **)
    758918let rec bebit_rect_Type3 h_BBbit h_BBundef h_BBptrcarry = function
    759 | BBbit x_5996 -> h_BBbit x_5996
     919| BBbit x_6396 -> h_BBbit x_6396
    760920| BBundef -> h_BBundef
    761 | BBptrcarry (x_5999, x_5998, p, x_5997) ->
    762   h_BBptrcarry x_5999 x_5998 p x_5997
     921| BBptrcarry (x_6399, x_6398, p, x_6397) ->
     922  h_BBptrcarry x_6399 x_6398 p x_6397
    763923
    764924(** val bebit_rect_Type2 :
     
    766926    BitVector.bitVector -> 'a1) -> bebit -> 'a1 **)
    767927let rec bebit_rect_Type2 h_BBbit h_BBundef h_BBptrcarry = function
    768 | BBbit x_6004 -> h_BBbit x_6004
     928| BBbit x_6404 -> h_BBbit x_6404
    769929| BBundef -> h_BBundef
    770 | BBptrcarry (x_6007, x_6006, p, x_6005) ->
    771   h_BBptrcarry x_6007 x_6006 p x_6005
     930| BBptrcarry (x_6407, x_6406, p, x_6405) ->
     931  h_BBptrcarry x_6407 x_6406 p x_6405
    772932
    773933(** val bebit_rect_Type1 :
     
    775935    BitVector.bitVector -> 'a1) -> bebit -> 'a1 **)
    776936let rec bebit_rect_Type1 h_BBbit h_BBundef h_BBptrcarry = function
    777 | BBbit x_6012 -> h_BBbit x_6012
     937| BBbit x_6412 -> h_BBbit x_6412
    778938| BBundef -> h_BBundef
    779 | BBptrcarry (x_6015, x_6014, p, x_6013) ->
    780   h_BBptrcarry x_6015 x_6014 p x_6013
     939| BBptrcarry (x_6415, x_6414, p, x_6413) ->
     940  h_BBptrcarry x_6415 x_6414 p x_6413
    781941
    782942(** val bebit_rect_Type0 :
     
    784944    BitVector.bitVector -> 'a1) -> bebit -> 'a1 **)
    785945let rec bebit_rect_Type0 h_BBbit h_BBundef h_BBptrcarry = function
    786 | BBbit x_6020 -> h_BBbit x_6020
     946| BBbit x_6420 -> h_BBbit x_6420
    787947| BBundef -> h_BBundef
    788 | BBptrcarry (x_6023, x_6022, p, x_6021) ->
    789   h_BBptrcarry x_6023 x_6022 p x_6021
     948| BBptrcarry (x_6423, x_6422, p, x_6421) ->
     949  h_BBptrcarry x_6423 x_6422 p x_6421
    790950
    791951(** val bebit_inv_rect_Type4 :
Note: See TracChangeset for help on using the changeset viewer.