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/backEndOps.ml

    r2730 r2743  
    402402    -> (BitVector.bit -> op2 -> BitVector.byte -> BitVector.byte ->
    403403    (BitVector.byte, BitVector.bit) Types.prod) -> 'a1) -> eval -> 'a1 **)
    404 let rec eval_rect_Type4 h_mk_Eval x_6259 =
    405   let { opaccs = opaccs0; op0 = op4; op3 = op5 } = x_6259 in
     404let rec eval_rect_Type4 h_mk_Eval x_18831 =
     405  let { opaccs = opaccs0; op0 = op4; op3 = op5 } = x_18831 in
    406406  h_mk_Eval opaccs0 op4 op5
    407407
     
    411411    -> (BitVector.bit -> op2 -> BitVector.byte -> BitVector.byte ->
    412412    (BitVector.byte, BitVector.bit) Types.prod) -> 'a1) -> eval -> 'a1 **)
    413 let rec eval_rect_Type5 h_mk_Eval x_6261 =
    414   let { opaccs = opaccs0; op0 = op4; op3 = op5 } = x_6261 in
     413let rec eval_rect_Type5 h_mk_Eval x_18833 =
     414  let { opaccs = opaccs0; op0 = op4; op3 = op5 } = x_18833 in
    415415  h_mk_Eval opaccs0 op4 op5
    416416
     
    420420    -> (BitVector.bit -> op2 -> BitVector.byte -> BitVector.byte ->
    421421    (BitVector.byte, BitVector.bit) Types.prod) -> 'a1) -> eval -> 'a1 **)
    422 let rec eval_rect_Type3 h_mk_Eval x_6263 =
    423   let { opaccs = opaccs0; op0 = op4; op3 = op5 } = x_6263 in
     422let rec eval_rect_Type3 h_mk_Eval x_18835 =
     423  let { opaccs = opaccs0; op0 = op4; op3 = op5 } = x_18835 in
    424424  h_mk_Eval opaccs0 op4 op5
    425425
     
    429429    -> (BitVector.bit -> op2 -> BitVector.byte -> BitVector.byte ->
    430430    (BitVector.byte, BitVector.bit) Types.prod) -> 'a1) -> eval -> 'a1 **)
    431 let rec eval_rect_Type2 h_mk_Eval x_6265 =
    432   let { opaccs = opaccs0; op0 = op4; op3 = op5 } = x_6265 in
     431let rec eval_rect_Type2 h_mk_Eval x_18837 =
     432  let { opaccs = opaccs0; op0 = op4; op3 = op5 } = x_18837 in
    433433  h_mk_Eval opaccs0 op4 op5
    434434
     
    438438    -> (BitVector.bit -> op2 -> BitVector.byte -> BitVector.byte ->
    439439    (BitVector.byte, BitVector.bit) Types.prod) -> 'a1) -> eval -> 'a1 **)
    440 let rec eval_rect_Type1 h_mk_Eval x_6267 =
    441   let { opaccs = opaccs0; op0 = op4; op3 = op5 } = x_6267 in
     440let rec eval_rect_Type1 h_mk_Eval x_18839 =
     441  let { opaccs = opaccs0; op0 = op4; op3 = op5 } = x_18839 in
    442442  h_mk_Eval opaccs0 op4 op5
    443443
     
    447447    -> (BitVector.bit -> op2 -> BitVector.byte -> BitVector.byte ->
    448448    (BitVector.byte, BitVector.bit) Types.prod) -> 'a1) -> eval -> 'a1 **)
    449 let rec eval_rect_Type0 h_mk_Eval x_6269 =
    450   let { opaccs = opaccs0; op0 = op4; op3 = op5 } = x_6269 in
     449let rec eval_rect_Type0 h_mk_Eval x_18841 =
     450  let { opaccs = opaccs0; op0 = op4; op3 = op5 } = x_18841 in
    451451  h_mk_Eval opaccs0 op4 op5
    452452
Note: See TracChangeset for help on using the changeset viewer.