Changeset 2743 for extracted/division.ml


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

    r2717 r2743  
    2828let rec natp_rect_Type4 h_pzero h_ppos = function
    2929| Pzero -> h_pzero
    30 | Ppos x_4823 -> h_ppos x_4823
     30| Ppos x_4849 -> h_ppos x_4849
    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_4827 -> h_ppos x_4827
     35| Ppos x_4853 -> h_ppos x_4853
    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_4831 -> h_ppos x_4831
     40| Ppos x_4857 -> h_ppos x_4857
    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_4835 -> h_ppos x_4835
     45| Ppos x_4861 -> h_ppos x_4861
    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_4839 -> h_ppos x_4839
     50| Ppos x_4865 -> h_ppos x_4865
    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_4843 -> h_ppos x_4843
     55| Ppos x_4869 -> h_ppos x_4869
    5656
    5757(** val natp_inv_rect_Type4 :
Note: See TracChangeset for help on using the changeset viewer.