Changeset 2649 for extracted/division.ml
 Timestamp:
 Feb 7, 2013, 10:43:49 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

extracted/division.ml
r2601 r2649 28 28 let rec natp_rect_Type4 h_pzero h_ppos = function 29 29  Pzero > h_pzero 30  Ppos x_ 3822 > h_ppos x_382230  Ppos x_4693 > h_ppos x_4693 31 31 32 32 (** val natp_rect_Type5 : 'a1 > (Positive.pos > 'a1) > natp > 'a1 **) 33 33 let rec natp_rect_Type5 h_pzero h_ppos = function 34 34  Pzero > h_pzero 35  Ppos x_ 3826 > h_ppos x_382635  Ppos x_4697 > h_ppos x_4697 36 36 37 37 (** val natp_rect_Type3 : 'a1 > (Positive.pos > 'a1) > natp > 'a1 **) 38 38 let rec natp_rect_Type3 h_pzero h_ppos = function 39 39  Pzero > h_pzero 40  Ppos x_ 3830 > h_ppos x_383040  Ppos x_4701 > h_ppos x_4701 41 41 42 42 (** val natp_rect_Type2 : 'a1 > (Positive.pos > 'a1) > natp > 'a1 **) 43 43 let rec natp_rect_Type2 h_pzero h_ppos = function 44 44  Pzero > h_pzero 45  Ppos x_ 3834 > h_ppos x_383445  Ppos x_4705 > h_ppos x_4705 46 46 47 47 (** val natp_rect_Type1 : 'a1 > (Positive.pos > 'a1) > natp > 'a1 **) 48 48 let rec natp_rect_Type1 h_pzero h_ppos = function 49 49  Pzero > h_pzero 50  Ppos x_ 3838 > h_ppos x_383850  Ppos x_4709 > h_ppos x_4709 51 51 52 52 (** val natp_rect_Type0 : 'a1 > (Positive.pos > 'a1) > natp > 'a1 **) 53 53 let rec natp_rect_Type0 h_pzero h_ppos = function 54 54  Pzero > h_pzero 55  Ppos x_ 3842 > h_ppos x_384255  Ppos x_4713 > h_ppos x_4713 56 56 57 57 (** val natp_inv_rect_Type4 :
Note: See TracChangeset
for help on using the changeset viewer.