Changeset 2717 for extracted/deqsets.ml


Ignore:
Timestamp:
Feb 23, 2013, 1:16:55 AM (7 years ago)
Author:
sacerdot
Message:

Extracted code for the whole compiler.
The space cost model is not there yet.

I have fixed by hand the few extraction problems
(i.e. composed coercions not extracted and type
definitions with wrong syntax).

I have also changed all axioms to be implemented
so that they do not fail at initialization time.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/deqsets.ml

    r2649 r2717  
    2121(** val deqSet_rect_Type4 :
    2222    (__ -> (__ -> __ -> Bool.bool) -> __ -> 'a1) -> deqSet -> 'a1 **)
    23 let rec deqSet_rect_Type4 h_mk_DeqSet x_3057 =
    24   let eqb = x_3057 in h_mk_DeqSet __ eqb __
     23let rec deqSet_rect_Type4 h_mk_DeqSet x_3083 =
     24  let eqb = x_3083 in h_mk_DeqSet __ eqb __
    2525
    2626(** val deqSet_rect_Type5 :
    2727    (__ -> (__ -> __ -> Bool.bool) -> __ -> 'a1) -> deqSet -> 'a1 **)
    28 let rec deqSet_rect_Type5 h_mk_DeqSet x_3059 =
    29   let eqb = x_3059 in h_mk_DeqSet __ eqb __
     28let rec deqSet_rect_Type5 h_mk_DeqSet x_3085 =
     29  let eqb = x_3085 in h_mk_DeqSet __ eqb __
    3030
    3131(** val deqSet_rect_Type3 :
    3232    (__ -> (__ -> __ -> Bool.bool) -> __ -> 'a1) -> deqSet -> 'a1 **)
    33 let rec deqSet_rect_Type3 h_mk_DeqSet x_3061 =
    34   let eqb = x_3061 in h_mk_DeqSet __ eqb __
     33let rec deqSet_rect_Type3 h_mk_DeqSet x_3087 =
     34  let eqb = x_3087 in h_mk_DeqSet __ eqb __
    3535
    3636(** val deqSet_rect_Type2 :
    3737    (__ -> (__ -> __ -> Bool.bool) -> __ -> 'a1) -> deqSet -> 'a1 **)
    38 let rec deqSet_rect_Type2 h_mk_DeqSet x_3063 =
    39   let eqb = x_3063 in h_mk_DeqSet __ eqb __
     38let rec deqSet_rect_Type2 h_mk_DeqSet x_3089 =
     39  let eqb = x_3089 in h_mk_DeqSet __ eqb __
    4040
    4141(** val deqSet_rect_Type1 :
    4242    (__ -> (__ -> __ -> Bool.bool) -> __ -> 'a1) -> deqSet -> 'a1 **)
    43 let rec deqSet_rect_Type1 h_mk_DeqSet x_3065 =
    44   let eqb = x_3065 in h_mk_DeqSet __ eqb __
     43let rec deqSet_rect_Type1 h_mk_DeqSet x_3091 =
     44  let eqb = x_3091 in h_mk_DeqSet __ eqb __
    4545
    4646(** val deqSet_rect_Type0 :
    4747    (__ -> (__ -> __ -> Bool.bool) -> __ -> 'a1) -> deqSet -> 'a1 **)
    48 let rec deqSet_rect_Type0 h_mk_DeqSet x_3067 =
    49   let eqb = x_3067 in h_mk_DeqSet __ eqb __
     48let rec deqSet_rect_Type0 h_mk_DeqSet x_3093 =
     49  let eqb = x_3093 in h_mk_DeqSet __ eqb __
    5050
    5151type carr = __
Note: See TracChangeset for help on using the changeset viewer.