Ignore:
Timestamp:
Mar 29, 2013, 6:38:26 PM (7 years ago)
Author:
sacerdot
Message:

New major extraction that should have solved all remaining issues.
As tests/PROBLEMI shows, we still have some bugs with:

a) initialization of global data (regression)
b) function pointers call

File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/arithmetic.ml

    r3033 r3043  
    297297(** val fbs_diff_rect_Type4 :
    298298    (Nat.nat -> Nat.nat -> 'a1) -> Nat.nat -> fbs_diff -> 'a1 **)
    299 let rec fbs_diff_rect_Type4 h_fbs_diff' x_4 = function
     299let rec fbs_diff_rect_Type4 h_fbs_diff' x_1368 = function
    300300| Fbs_diff' (n, m) -> h_fbs_diff' n m
    301301
    302302(** val fbs_diff_rect_Type5 :
    303303    (Nat.nat -> Nat.nat -> 'a1) -> Nat.nat -> fbs_diff -> 'a1 **)
    304 let rec fbs_diff_rect_Type5 h_fbs_diff' x_7 = function
     304let rec fbs_diff_rect_Type5 h_fbs_diff' x_1371 = function
    305305| Fbs_diff' (n, m) -> h_fbs_diff' n m
    306306
    307307(** val fbs_diff_rect_Type3 :
    308308    (Nat.nat -> Nat.nat -> 'a1) -> Nat.nat -> fbs_diff -> 'a1 **)
    309 let rec fbs_diff_rect_Type3 h_fbs_diff' x_10 = function
     309let rec fbs_diff_rect_Type3 h_fbs_diff' x_1374 = function
    310310| Fbs_diff' (n, m) -> h_fbs_diff' n m
    311311
    312312(** val fbs_diff_rect_Type2 :
    313313    (Nat.nat -> Nat.nat -> 'a1) -> Nat.nat -> fbs_diff -> 'a1 **)
    314 let rec fbs_diff_rect_Type2 h_fbs_diff' x_13 = function
     314let rec fbs_diff_rect_Type2 h_fbs_diff' x_1377 = function
    315315| Fbs_diff' (n, m) -> h_fbs_diff' n m
    316316
    317317(** val fbs_diff_rect_Type1 :
    318318    (Nat.nat -> Nat.nat -> 'a1) -> Nat.nat -> fbs_diff -> 'a1 **)
    319 let rec fbs_diff_rect_Type1 h_fbs_diff' x_16 = function
     319let rec fbs_diff_rect_Type1 h_fbs_diff' x_1380 = function
    320320| Fbs_diff' (n, m) -> h_fbs_diff' n m
    321321
    322322(** val fbs_diff_rect_Type0 :
    323323    (Nat.nat -> Nat.nat -> 'a1) -> Nat.nat -> fbs_diff -> 'a1 **)
    324 let rec fbs_diff_rect_Type0 h_fbs_diff' x_19 = function
     324let rec fbs_diff_rect_Type0 h_fbs_diff' x_1383 = function
    325325| Fbs_diff' (n, m) -> h_fbs_diff' n m
    326326
Note: See TracChangeset for help on using the changeset viewer.