Changeset 3043 for extracted/division.ml


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

    r2827 r3043  
    2828let rec natp_rect_Type4 h_pzero h_ppos = function
    2929| Pzero -> h_pzero
    30 | Ppos x_4888 -> h_ppos x_4888
     30| Ppos x_4901 -> h_ppos x_4901
    3131
    3232(** val natp_rect_Type5 : 'a1 -> (Positive.pos -> 'a1) -> natp -> 'a1 **)
    3333let rec natp_rect_Type5 h_pzero h_ppos = function
    3434| Pzero -> h_pzero
    35 | Ppos x_4892 -> h_ppos x_4892
     35| Ppos x_4905 -> h_ppos x_4905
    3636
    3737(** val natp_rect_Type3 : 'a1 -> (Positive.pos -> 'a1) -> natp -> 'a1 **)
    3838let rec natp_rect_Type3 h_pzero h_ppos = function
    3939| Pzero -> h_pzero
    40 | Ppos x_4896 -> h_ppos x_4896
     40| Ppos x_4909 -> h_ppos x_4909
    4141
    4242(** val natp_rect_Type2 : 'a1 -> (Positive.pos -> 'a1) -> natp -> 'a1 **)
    4343let rec natp_rect_Type2 h_pzero h_ppos = function
    4444| Pzero -> h_pzero
    45 | Ppos x_4900 -> h_ppos x_4900
     45| Ppos x_4913 -> h_ppos x_4913
    4646
    4747(** val natp_rect_Type1 : 'a1 -> (Positive.pos -> 'a1) -> natp -> 'a1 **)
    4848let rec natp_rect_Type1 h_pzero h_ppos = function
    4949| Pzero -> h_pzero
    50 | Ppos x_4904 -> h_ppos x_4904
     50| Ppos x_4917 -> h_ppos x_4917
    5151
    5252(** val natp_rect_Type0 : 'a1 -> (Positive.pos -> 'a1) -> natp -> 'a1 **)
    5353let rec natp_rect_Type0 h_pzero h_ppos = function
    5454| Pzero -> h_pzero
    55 | Ppos x_4908 -> h_ppos x_4908
     55| Ppos x_4921 -> h_ppos x_4921
    5656
    5757(** val natp_inv_rect_Type4 :
Note: See TracChangeset for help on using the changeset viewer.