Changeset 2773 for extracted/jmeq.ml


Ignore:
Timestamp:
Mar 4, 2013, 10:03:33 AM (7 years ago)
Author:
sacerdot
Message:
  1. everything extracted again after all bugs in Matita's extraction have been fixed. No more need for manual patching
  2. new extraction after file reorganization (by James)
File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/jmeq.ml

    r2601 r2773  
    1414
    1515(** val sigma_rect_Type4 : (__ -> __ -> 'a1) -> sigma -> 'a1 **)
    16 let rec sigma_rect_Type4 h_mk_Sigma x_890 =
    17   let x_891 = x_890 in h_mk_Sigma __ x_891
     16let rec sigma_rect_Type4 h_mk_Sigma x_812 =
     17  let x_813 = x_812 in h_mk_Sigma __ x_813
    1818
    1919(** val sigma_rect_Type5 : (__ -> __ -> 'a1) -> sigma -> 'a1 **)
    20 let rec sigma_rect_Type5 h_mk_Sigma x_893 =
    21   let x_894 = x_893 in h_mk_Sigma __ x_894
     20let rec sigma_rect_Type5 h_mk_Sigma x_815 =
     21  let x_816 = x_815 in h_mk_Sigma __ x_816
    2222
    2323(** val sigma_rect_Type3 : (__ -> __ -> 'a1) -> sigma -> 'a1 **)
    24 let rec sigma_rect_Type3 h_mk_Sigma x_896 =
    25   let x_897 = x_896 in h_mk_Sigma __ x_897
     24let rec sigma_rect_Type3 h_mk_Sigma x_818 =
     25  let x_819 = x_818 in h_mk_Sigma __ x_819
    2626
    2727(** val sigma_rect_Type2 : (__ -> __ -> 'a1) -> sigma -> 'a1 **)
    28 let rec sigma_rect_Type2 h_mk_Sigma x_899 =
    29   let x_900 = x_899 in h_mk_Sigma __ x_900
     28let rec sigma_rect_Type2 h_mk_Sigma x_821 =
     29  let x_822 = x_821 in h_mk_Sigma __ x_822
    3030
    3131(** val sigma_rect_Type1 : (__ -> __ -> 'a1) -> sigma -> 'a1 **)
    32 let rec sigma_rect_Type1 h_mk_Sigma x_902 =
    33   let x_903 = x_902 in h_mk_Sigma __ x_903
     32let rec sigma_rect_Type1 h_mk_Sigma x_824 =
     33  let x_825 = x_824 in h_mk_Sigma __ x_825
    3434
    3535(** val sigma_rect_Type0 : (__ -> __ -> 'a1) -> sigma -> 'a1 **)
    36 let rec sigma_rect_Type0 h_mk_Sigma x_905 =
    37   let x_906 = x_905 in h_mk_Sigma __ x_906
     36let rec sigma_rect_Type0 h_mk_Sigma x_827 =
     37  let x_828 = x_827 in h_mk_Sigma __ x_828
    3838
    3939(** val sigma_inv_rect_Type4 : sigma -> (__ -> __ -> __ -> 'a1) -> 'a1 **)
     
    6464
    6565(** val jmeq_rect_Type4 : 'a1 -> 'a2 -> 'a3 -> 'a2 **)
    66 let rec jmeq_rect_Type4 x h_refl_jmeq x_929 =
     66let rec jmeq_rect_Type4 x h_refl_jmeq x_851 =
    6767  h_refl_jmeq
    6868
    6969(** val jmeq_rect_Type5 : 'a1 -> 'a2 -> 'a3 -> 'a2 **)
    70 let rec jmeq_rect_Type5 x h_refl_jmeq x_932 =
     70let rec jmeq_rect_Type5 x h_refl_jmeq x_854 =
    7171  h_refl_jmeq
    7272
    7373(** val jmeq_rect_Type3 : 'a1 -> 'a2 -> 'a3 -> 'a2 **)
    74 let rec jmeq_rect_Type3 x h_refl_jmeq x_935 =
     74let rec jmeq_rect_Type3 x h_refl_jmeq x_857 =
    7575  h_refl_jmeq
    7676
    7777(** val jmeq_rect_Type2 : 'a1 -> 'a2 -> 'a3 -> 'a2 **)
    78 let rec jmeq_rect_Type2 x h_refl_jmeq x_938 =
     78let rec jmeq_rect_Type2 x h_refl_jmeq x_860 =
    7979  h_refl_jmeq
    8080
    8181(** val jmeq_rect_Type1 : 'a1 -> 'a2 -> 'a3 -> 'a2 **)
    82 let rec jmeq_rect_Type1 x h_refl_jmeq x_941 =
     82let rec jmeq_rect_Type1 x h_refl_jmeq x_863 =
    8383  h_refl_jmeq
    8484
    8585(** val jmeq_rect_Type0 : 'a1 -> 'a2 -> 'a3 -> 'a2 **)
    86 let rec jmeq_rect_Type0 x h_refl_jmeq x_944 =
     86let rec jmeq_rect_Type0 x h_refl_jmeq x_866 =
    8787  h_refl_jmeq
    8888
Note: See TracChangeset for help on using the changeset viewer.