Ignore:
Timestamp:
Mar 21, 2013, 8:11:50 PM (6 years ago)
Author:
sacerdot
Message:

New extraction, several bug fixed. RTL_semantics fixed by hand, will be fixed
automatically when Paolo commits.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/byteValues.ml

    r2827 r2933  
    8989    (Pointers.block Types.sig0 -> Positive.pos -> 'a1) -> program_counter ->
    9090    'a1 **)
    91 let rec program_counter_rect_Type4 h_mk_program_counter x_6139 =
    92   let { pc_block = pc_block0; pc_offset = pc_offset0 } = x_6139 in
     91let rec program_counter_rect_Type4 h_mk_program_counter x_3 =
     92  let { pc_block = pc_block0; pc_offset = pc_offset0 } = x_3 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_6141 =
    99   let { pc_block = pc_block0; pc_offset = pc_offset0 } = x_6141 in
     98let rec program_counter_rect_Type5 h_mk_program_counter x_5 =
     99  let { pc_block = pc_block0; pc_offset = pc_offset0 } = x_5 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_6143 =
    106   let { pc_block = pc_block0; pc_offset = pc_offset0 } = x_6143 in
     105let rec program_counter_rect_Type3 h_mk_program_counter x_7 =
     106  let { pc_block = pc_block0; pc_offset = pc_offset0 } = x_7 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_6145 =
    113   let { pc_block = pc_block0; pc_offset = pc_offset0 } = x_6145 in
     112let rec program_counter_rect_Type2 h_mk_program_counter x_9 =
     113  let { pc_block = pc_block0; pc_offset = pc_offset0 } = x_9 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_6147 =
    120   let { pc_block = pc_block0; pc_offset = pc_offset0 } = x_6147 in
     119let rec program_counter_rect_Type1 h_mk_program_counter x_11 =
     120  let { pc_block = pc_block0; pc_offset = pc_offset0 } = x_11 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_6149 =
    127   let { pc_block = pc_block0; pc_offset = pc_offset0 } = x_6149 in
     126let rec program_counter_rect_Type0 h_mk_program_counter x_13 =
     127  let { pc_block = pc_block0; pc_offset = pc_offset0 } = x_13 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_6165 =
    218   let part_no = x_6165 in h_mk_part part_no __
     217let rec part_rect_Type4 h_mk_part x_29 =
     218  let part_no = x_29 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_6167 =
    222   let part_no = x_6167 in h_mk_part part_no __
     221let rec part_rect_Type5 h_mk_part x_31 =
     222  let part_no = x_31 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_6169 =
    226   let part_no = x_6169 in h_mk_part part_no __
     225let rec part_rect_Type3 h_mk_part x_33 =
     226  let part_no = x_33 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_6171 =
    230   let part_no = x_6171 in h_mk_part part_no __
     229let rec part_rect_Type2 h_mk_part x_35 =
     230  let part_no = x_35 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_6173 =
    234   let part_no = x_6173 in h_mk_part part_no __
     233let rec part_rect_Type1 h_mk_part x_37 =
     234  let part_no = x_37 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_6175 =
    238   let part_no = x_6175 in h_mk_part part_no __
     237let rec part_rect_Type0 h_mk_part x_39 =
     238  let part_no = x_39 in h_mk_part part_no __
    239239
    240240(** val part_no : part -> Nat.nat **)
     
    486486| BVundef -> h_BVundef
    487487| BVnonzero -> h_BVnonzero
    488 | BVXor (x_6209, x_6208, x_6207) -> h_BVXor x_6209 x_6208 x_6207
    489 | BVByte x_6210 -> h_BVByte x_6210
    490 | BVnull x_6211 -> h_BVnull x_6211
    491 | BVptr (x_6213, x_6212) -> h_BVptr x_6213 x_6212
    492 | BVpc (x_6215, x_6214) -> h_BVpc x_6215 x_6214
     488| BVXor (x_73, x_72, x_71) -> h_BVXor x_73 x_72 x_71
     489| BVByte x_74 -> h_BVByte x_74
     490| BVnull x_75 -> h_BVnull x_75
     491| BVptr (x_77, x_76) -> h_BVptr x_77 x_76
     492| BVpc (x_79, x_78) -> h_BVpc x_79 x_78
    493493
    494494(** val beval_rect_Type5 :
     
    500500| BVundef -> h_BVundef
    501501| BVnonzero -> h_BVnonzero
    502 | BVXor (x_6226, x_6225, x_6224) -> h_BVXor x_6226 x_6225 x_6224
    503 | BVByte x_6227 -> h_BVByte x_6227
    504 | BVnull x_6228 -> h_BVnull x_6228
    505 | BVptr (x_6230, x_6229) -> h_BVptr x_6230 x_6229
    506 | BVpc (x_6232, x_6231) -> h_BVpc x_6232 x_6231
     502| BVXor (x_90, x_89, x_88) -> h_BVXor x_90 x_89 x_88
     503| BVByte x_91 -> h_BVByte x_91
     504| BVnull x_92 -> h_BVnull x_92
     505| BVptr (x_94, x_93) -> h_BVptr x_94 x_93
     506| BVpc (x_96, x_95) -> h_BVpc x_96 x_95
    507507
    508508(** val beval_rect_Type3 :
     
    514514| BVundef -> h_BVundef
    515515| BVnonzero -> h_BVnonzero
    516 | BVXor (x_6243, x_6242, x_6241) -> h_BVXor x_6243 x_6242 x_6241
    517 | BVByte x_6244 -> h_BVByte x_6244
    518 | BVnull x_6245 -> h_BVnull x_6245
    519 | BVptr (x_6247, x_6246) -> h_BVptr x_6247 x_6246
    520 | BVpc (x_6249, x_6248) -> h_BVpc x_6249 x_6248
     516| BVXor (x_107, x_106, x_105) -> h_BVXor x_107 x_106 x_105
     517| BVByte x_108 -> h_BVByte x_108
     518| BVnull x_109 -> h_BVnull x_109
     519| BVptr (x_111, x_110) -> h_BVptr x_111 x_110
     520| BVpc (x_113, x_112) -> h_BVpc x_113 x_112
    521521
    522522(** val beval_rect_Type2 :
     
    528528| BVundef -> h_BVundef
    529529| BVnonzero -> h_BVnonzero
    530 | BVXor (x_6260, x_6259, x_6258) -> h_BVXor x_6260 x_6259 x_6258
    531 | BVByte x_6261 -> h_BVByte x_6261
    532 | BVnull x_6262 -> h_BVnull x_6262
    533 | BVptr (x_6264, x_6263) -> h_BVptr x_6264 x_6263
    534 | BVpc (x_6266, x_6265) -> h_BVpc x_6266 x_6265
     530| BVXor (x_124, x_123, x_122) -> h_BVXor x_124 x_123 x_122
     531| BVByte x_125 -> h_BVByte x_125
     532| BVnull x_126 -> h_BVnull x_126
     533| BVptr (x_128, x_127) -> h_BVptr x_128 x_127
     534| BVpc (x_130, x_129) -> h_BVpc x_130 x_129
    535535
    536536(** val beval_rect_Type1 :
     
    542542| BVundef -> h_BVundef
    543543| BVnonzero -> h_BVnonzero
    544 | BVXor (x_6277, x_6276, x_6275) -> h_BVXor x_6277 x_6276 x_6275
    545 | BVByte x_6278 -> h_BVByte x_6278
    546 | BVnull x_6279 -> h_BVnull x_6279
    547 | BVptr (x_6281, x_6280) -> h_BVptr x_6281 x_6280
    548 | BVpc (x_6283, x_6282) -> h_BVpc x_6283 x_6282
     544| BVXor (x_141, x_140, x_139) -> h_BVXor x_141 x_140 x_139
     545| BVByte x_142 -> h_BVByte x_142
     546| BVnull x_143 -> h_BVnull x_143
     547| BVptr (x_145, x_144) -> h_BVptr x_145 x_144
     548| BVpc (x_147, x_146) -> h_BVpc x_147 x_146
    549549
    550550(** val beval_rect_Type0 :
     
    556556| BVundef -> h_BVundef
    557557| BVnonzero -> h_BVnonzero
    558 | BVXor (x_6294, x_6293, x_6292) -> h_BVXor x_6294 x_6293 x_6292
    559 | BVByte x_6295 -> h_BVByte x_6295
    560 | BVnull x_6296 -> h_BVnull x_6296
    561 | BVptr (x_6298, x_6297) -> h_BVptr x_6298 x_6297
    562 | BVpc (x_6300, x_6299) -> h_BVpc x_6300 x_6299
     558| BVXor (x_158, x_157, x_156) -> h_BVXor x_158 x_157 x_156
     559| BVByte x_159 -> h_BVByte x_159
     560| BVnull x_160 -> h_BVnull x_160
     561| BVptr (x_162, x_161) -> h_BVptr x_162 x_161
     562| BVpc (x_164, x_163) -> h_BVpc x_164 x_163
    563563
    564564(** val beval_inv_rect_Type4 :
     
    828828| BVByte b ->
    829829  Errors.OK
    830     (BitVector.eq_bv (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    831       Nat.O))))))))
    832       (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    833         Nat.O))))))))) b)
     830    (Bool.notb
     831      (BitVector.eq_bv (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     832        (Nat.S Nat.O))))))))
     833        (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
     834          (Nat.S Nat.O))))))))) b))
    834835| BVnull x -> Errors.OK Bool.False
    835836| BVptr (x, x0) -> Errors.OK Bool.True
     
    890891                ErrorMessages.NotAnInt32Val), List.Nil))))))))
    891892
     893type add_or_sub =
     894| Do_add
     895| Do_sub
     896
     897(** val add_or_sub_rect_Type4 : 'a1 -> 'a1 -> add_or_sub -> 'a1 **)
     898let rec add_or_sub_rect_Type4 h_do_add h_do_sub = function
     899| Do_add -> h_do_add
     900| Do_sub -> h_do_sub
     901
     902(** val add_or_sub_rect_Type5 : 'a1 -> 'a1 -> add_or_sub -> 'a1 **)
     903let rec add_or_sub_rect_Type5 h_do_add h_do_sub = function
     904| Do_add -> h_do_add
     905| Do_sub -> h_do_sub
     906
     907(** val add_or_sub_rect_Type3 : 'a1 -> 'a1 -> add_or_sub -> 'a1 **)
     908let rec add_or_sub_rect_Type3 h_do_add h_do_sub = function
     909| Do_add -> h_do_add
     910| Do_sub -> h_do_sub
     911
     912(** val add_or_sub_rect_Type2 : 'a1 -> 'a1 -> add_or_sub -> 'a1 **)
     913let rec add_or_sub_rect_Type2 h_do_add h_do_sub = function
     914| Do_add -> h_do_add
     915| Do_sub -> h_do_sub
     916
     917(** val add_or_sub_rect_Type1 : 'a1 -> 'a1 -> add_or_sub -> 'a1 **)
     918let rec add_or_sub_rect_Type1 h_do_add h_do_sub = function
     919| Do_add -> h_do_add
     920| Do_sub -> h_do_sub
     921
     922(** val add_or_sub_rect_Type0 : 'a1 -> 'a1 -> add_or_sub -> 'a1 **)
     923let rec add_or_sub_rect_Type0 h_do_add h_do_sub = function
     924| Do_add -> h_do_add
     925| Do_sub -> h_do_sub
     926
     927(** val add_or_sub_inv_rect_Type4 :
     928    add_or_sub -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
     929let add_or_sub_inv_rect_Type4 hterm h1 h2 =
     930  let hcut = add_or_sub_rect_Type4 h1 h2 hterm in hcut __
     931
     932(** val add_or_sub_inv_rect_Type3 :
     933    add_or_sub -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
     934let add_or_sub_inv_rect_Type3 hterm h1 h2 =
     935  let hcut = add_or_sub_rect_Type3 h1 h2 hterm in hcut __
     936
     937(** val add_or_sub_inv_rect_Type2 :
     938    add_or_sub -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
     939let add_or_sub_inv_rect_Type2 hterm h1 h2 =
     940  let hcut = add_or_sub_rect_Type2 h1 h2 hterm in hcut __
     941
     942(** val add_or_sub_inv_rect_Type1 :
     943    add_or_sub -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
     944let add_or_sub_inv_rect_Type1 hterm h1 h2 =
     945  let hcut = add_or_sub_rect_Type1 h1 h2 hterm in hcut __
     946
     947(** val add_or_sub_inv_rect_Type0 :
     948    add_or_sub -> (__ -> 'a1) -> (__ -> 'a1) -> 'a1 **)
     949let add_or_sub_inv_rect_Type0 hterm h1 h2 =
     950  let hcut = add_or_sub_rect_Type0 h1 h2 hterm in hcut __
     951
     952(** val add_or_sub_discr : add_or_sub -> add_or_sub -> __ **)
     953let add_or_sub_discr x y =
     954  Logic.eq_rect_Type2 x
     955    (match x with
     956     | Do_add -> Obj.magic (fun _ dH -> dH)
     957     | Do_sub -> Obj.magic (fun _ dH -> dH)) y
     958
     959(** val add_or_sub_jmdiscr : add_or_sub -> add_or_sub -> __ **)
     960let add_or_sub_jmdiscr x y =
     961  Logic.eq_rect_Type2 x
     962    (match x with
     963     | Do_add -> Obj.magic (fun _ dH -> dH)
     964     | Do_sub -> Obj.magic (fun _ dH -> dH)) y
     965
     966(** val eq_add_or_sub : add_or_sub -> add_or_sub -> Bool.bool **)
     967let eq_add_or_sub x y =
     968  match x with
     969  | Do_add ->
     970    (match y with
     971     | Do_add -> Bool.True
     972     | Do_sub -> Bool.False)
     973  | Do_sub ->
     974    (match y with
     975     | Do_add -> Bool.False
     976     | Do_sub -> Bool.True)
     977
    892978type bebit =
    893979| BBbit of Bool.bool
    894980| BBundef
    895 | BBptrcarry of Bool.bool * Pointers.pointer * part * BitVector.bitVector
     981| BBptrcarry of add_or_sub * Pointers.pointer * part * BitVector.bitVector
    896982
    897983(** val bebit_rect_Type4 :
    898     (Bool.bool -> 'a1) -> 'a1 -> (Bool.bool -> Pointers.pointer -> part ->
     984    (Bool.bool -> 'a1) -> 'a1 -> (add_or_sub -> Pointers.pointer -> part ->
    899985    BitVector.bitVector -> 'a1) -> bebit -> 'a1 **)
    900986let rec bebit_rect_Type4 h_BBbit h_BBundef h_BBptrcarry = function
    901 | BBbit x_6419 -> h_BBbit x_6419
     987| BBbit x_322 -> h_BBbit x_322
    902988| BBundef -> h_BBundef
    903 | BBptrcarry (x_6422, x_6421, p, x_6420) ->
    904   h_BBptrcarry x_6422 x_6421 p x_6420
     989| BBptrcarry (x_325, x_324, p, x_323) -> h_BBptrcarry x_325 x_324 p x_323
    905990
    906991(** val bebit_rect_Type5 :
    907     (Bool.bool -> 'a1) -> 'a1 -> (Bool.bool -> Pointers.pointer -> part ->
     992    (Bool.bool -> 'a1) -> 'a1 -> (add_or_sub -> Pointers.pointer -> part ->
    908993    BitVector.bitVector -> 'a1) -> bebit -> 'a1 **)
    909994let rec bebit_rect_Type5 h_BBbit h_BBundef h_BBptrcarry = function
    910 | BBbit x_6427 -> h_BBbit x_6427
     995| BBbit x_330 -> h_BBbit x_330
    911996| BBundef -> h_BBundef
    912 | BBptrcarry (x_6430, x_6429, p, x_6428) ->
    913   h_BBptrcarry x_6430 x_6429 p x_6428
     997| BBptrcarry (x_333, x_332, p, x_331) -> h_BBptrcarry x_333 x_332 p x_331
    914998
    915999(** val bebit_rect_Type3 :
    916     (Bool.bool -> 'a1) -> 'a1 -> (Bool.bool -> Pointers.pointer -> part ->
     1000    (Bool.bool -> 'a1) -> 'a1 -> (add_or_sub -> Pointers.pointer -> part ->
    9171001    BitVector.bitVector -> 'a1) -> bebit -> 'a1 **)
    9181002let rec bebit_rect_Type3 h_BBbit h_BBundef h_BBptrcarry = function
    919 | BBbit x_6435 -> h_BBbit x_6435
     1003| BBbit x_338 -> h_BBbit x_338
    9201004| BBundef -> h_BBundef
    921 | BBptrcarry (x_6438, x_6437, p, x_6436) ->
    922   h_BBptrcarry x_6438 x_6437 p x_6436
     1005| BBptrcarry (x_341, x_340, p, x_339) -> h_BBptrcarry x_341 x_340 p x_339
    9231006
    9241007(** val bebit_rect_Type2 :
    925     (Bool.bool -> 'a1) -> 'a1 -> (Bool.bool -> Pointers.pointer -> part ->
     1008    (Bool.bool -> 'a1) -> 'a1 -> (add_or_sub -> Pointers.pointer -> part ->
    9261009    BitVector.bitVector -> 'a1) -> bebit -> 'a1 **)
    9271010let rec bebit_rect_Type2 h_BBbit h_BBundef h_BBptrcarry = function
    928 | BBbit x_6443 -> h_BBbit x_6443
     1011| BBbit x_346 -> h_BBbit x_346
    9291012| BBundef -> h_BBundef
    930 | BBptrcarry (x_6446, x_6445, p, x_6444) ->
    931   h_BBptrcarry x_6446 x_6445 p x_6444
     1013| BBptrcarry (x_349, x_348, p, x_347) -> h_BBptrcarry x_349 x_348 p x_347
    9321014
    9331015(** val bebit_rect_Type1 :
    934     (Bool.bool -> 'a1) -> 'a1 -> (Bool.bool -> Pointers.pointer -> part ->
     1016    (Bool.bool -> 'a1) -> 'a1 -> (add_or_sub -> Pointers.pointer -> part ->
    9351017    BitVector.bitVector -> 'a1) -> bebit -> 'a1 **)
    9361018let rec bebit_rect_Type1 h_BBbit h_BBundef h_BBptrcarry = function
    937 | BBbit x_6451 -> h_BBbit x_6451
     1019| BBbit x_354 -> h_BBbit x_354
    9381020| BBundef -> h_BBundef
    939 | BBptrcarry (x_6454, x_6453, p, x_6452) ->
    940   h_BBptrcarry x_6454 x_6453 p x_6452
     1021| BBptrcarry (x_357, x_356, p, x_355) -> h_BBptrcarry x_357 x_356 p x_355
    9411022
    9421023(** val bebit_rect_Type0 :
    943     (Bool.bool -> 'a1) -> 'a1 -> (Bool.bool -> Pointers.pointer -> part ->
     1024    (Bool.bool -> 'a1) -> 'a1 -> (add_or_sub -> Pointers.pointer -> part ->
    9441025    BitVector.bitVector -> 'a1) -> bebit -> 'a1 **)
    9451026let rec bebit_rect_Type0 h_BBbit h_BBundef h_BBptrcarry = function
    946 | BBbit x_6459 -> h_BBbit x_6459
     1027| BBbit x_362 -> h_BBbit x_362
    9471028| BBundef -> h_BBundef
    948 | BBptrcarry (x_6462, x_6461, p, x_6460) ->
    949   h_BBptrcarry x_6462 x_6461 p x_6460
     1029| BBptrcarry (x_365, x_364, p, x_363) -> h_BBptrcarry x_365 x_364 p x_363
    9501030
    9511031(** val bebit_inv_rect_Type4 :
    952     bebit -> (Bool.bool -> __ -> 'a1) -> (__ -> 'a1) -> (Bool.bool ->
     1032    bebit -> (Bool.bool -> __ -> 'a1) -> (__ -> 'a1) -> (add_or_sub ->
    9531033    Pointers.pointer -> part -> BitVector.bitVector -> __ -> 'a1) -> 'a1 **)
    9541034let bebit_inv_rect_Type4 hterm h1 h2 h3 =
     
    9561036
    9571037(** val bebit_inv_rect_Type3 :
    958     bebit -> (Bool.bool -> __ -> 'a1) -> (__ -> 'a1) -> (Bool.bool ->
     1038    bebit -> (Bool.bool -> __ -> 'a1) -> (__ -> 'a1) -> (add_or_sub ->
    9591039    Pointers.pointer -> part -> BitVector.bitVector -> __ -> 'a1) -> 'a1 **)
    9601040let bebit_inv_rect_Type3 hterm h1 h2 h3 =
     
    9621042
    9631043(** val bebit_inv_rect_Type2 :
    964     bebit -> (Bool.bool -> __ -> 'a1) -> (__ -> 'a1) -> (Bool.bool ->
     1044    bebit -> (Bool.bool -> __ -> 'a1) -> (__ -> 'a1) -> (add_or_sub ->
    9651045    Pointers.pointer -> part -> BitVector.bitVector -> __ -> 'a1) -> 'a1 **)
    9661046let bebit_inv_rect_Type2 hterm h1 h2 h3 =
     
    9681048
    9691049(** val bebit_inv_rect_Type1 :
    970     bebit -> (Bool.bool -> __ -> 'a1) -> (__ -> 'a1) -> (Bool.bool ->
     1050    bebit -> (Bool.bool -> __ -> 'a1) -> (__ -> 'a1) -> (add_or_sub ->
    9711051    Pointers.pointer -> part -> BitVector.bitVector -> __ -> 'a1) -> 'a1 **)
    9721052let bebit_inv_rect_Type1 hterm h1 h2 h3 =
     
    9741054
    9751055(** val bebit_inv_rect_Type0 :
    976     bebit -> (Bool.bool -> __ -> 'a1) -> (__ -> 'a1) -> (Bool.bool ->
     1056    bebit -> (Bool.bool -> __ -> 'a1) -> (__ -> 'a1) -> (add_or_sub ->
    9771057    Pointers.pointer -> part -> BitVector.bitVector -> __ -> 'a1) -> 'a1 **)
    9781058let bebit_inv_rect_Type0 hterm h1 h2 h3 =
Note: See TracChangeset for help on using the changeset viewer.