Changeset 2797 for extracted/z.ml


Ignore:
Timestamp:
Mar 7, 2013, 12:55:34 PM (7 years ago)
Author:
sacerdot
Message:

Extracted again after James's cleanup and the implementation of the
new testing function to be used in the untrusted code.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/z.ml

    r2775 r2797  
    2626let rec z_rect_Type4 h_OZ h_pos h_neg = function
    2727| OZ -> h_OZ
    28 | Pos x_4643 -> h_pos x_4643
    29 | Neg x_4644 -> h_neg x_4644
     28| Pos x_4656 -> h_pos x_4656
     29| Neg x_4657 -> h_neg x_4657
    3030
    3131(** val z_rect_Type5 :
     
    3333let rec z_rect_Type5 h_OZ h_pos h_neg = function
    3434| OZ -> h_OZ
    35 | Pos x_4649 -> h_pos x_4649
    36 | Neg x_4650 -> h_neg x_4650
     35| Pos x_4662 -> h_pos x_4662
     36| Neg x_4663 -> h_neg x_4663
    3737
    3838(** val z_rect_Type3 :
     
    4040let rec z_rect_Type3 h_OZ h_pos h_neg = function
    4141| OZ -> h_OZ
    42 | Pos x_4655 -> h_pos x_4655
    43 | Neg x_4656 -> h_neg x_4656
     42| Pos x_4668 -> h_pos x_4668
     43| Neg x_4669 -> h_neg x_4669
    4444
    4545(** val z_rect_Type2 :
     
    4747let rec z_rect_Type2 h_OZ h_pos h_neg = function
    4848| OZ -> h_OZ
    49 | Pos x_4661 -> h_pos x_4661
    50 | Neg x_4662 -> h_neg x_4662
     49| Pos x_4674 -> h_pos x_4674
     50| Neg x_4675 -> h_neg x_4675
    5151
    5252(** val z_rect_Type1 :
     
    5454let rec z_rect_Type1 h_OZ h_pos h_neg = function
    5555| OZ -> h_OZ
    56 | Pos x_4667 -> h_pos x_4667
    57 | Neg x_4668 -> h_neg x_4668
     56| Pos x_4680 -> h_pos x_4680
     57| Neg x_4681 -> h_neg x_4681
    5858
    5959(** val z_rect_Type0 :
     
    6161let rec z_rect_Type0 h_OZ h_pos h_neg = function
    6262| OZ -> h_OZ
    63 | Pos x_4673 -> h_pos x_4673
    64 | Neg x_4674 -> h_neg x_4674
     63| Pos x_4686 -> h_pos x_4686
     64| Neg x_4687 -> h_neg x_4687
    6565
    6666(** val z_inv_rect_Type4 :
Note: See TracChangeset for help on using the changeset viewer.