Changeset 2649 for extracted/values.ml


Ignore:
Timestamp:
Feb 7, 2013, 10:43:49 PM (7 years ago)
Author:
sacerdot
Message:

...

File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/values.ml

    r2601 r2649  
    2929open Coqlib
    3030
     31open ErrorMessages
     32
    3133open Option
    3234
     
    3739open Positive
    3840
    39 open Char
    40 
    41 open String
    42 
    4341open PreIdentifiers
    4442
     
    5654
    5755open Identifiers
    58 
    59 open Floats
    6056
    6157open Integers
     
    9288let rec val_rect_Type4 h_Vundef h_Vint h_Vnull h_Vptr = function
    9389| Vundef -> h_Vundef
    94 | Vint (sz, x_4033) -> h_Vint sz x_4033
     90| Vint (sz, x_2472) -> h_Vint sz x_2472
    9591| Vnull -> h_Vnull
    96 | Vptr x_4034 -> h_Vptr x_4034
     92| Vptr x_2473 -> h_Vptr x_2473
    9793
    9894(** val val_rect_Type5 :
     
    10197let rec val_rect_Type5 h_Vundef h_Vint h_Vnull h_Vptr = function
    10298| Vundef -> h_Vundef
    103 | Vint (sz, x_4040) -> h_Vint sz x_4040
     99| Vint (sz, x_2479) -> h_Vint sz x_2479
    104100| Vnull -> h_Vnull
    105 | Vptr x_4041 -> h_Vptr x_4041
     101| Vptr x_2480 -> h_Vptr x_2480
    106102
    107103(** val val_rect_Type3 :
     
    110106let rec val_rect_Type3 h_Vundef h_Vint h_Vnull h_Vptr = function
    111107| Vundef -> h_Vundef
    112 | Vint (sz, x_4047) -> h_Vint sz x_4047
     108| Vint (sz, x_2486) -> h_Vint sz x_2486
    113109| Vnull -> h_Vnull
    114 | Vptr x_4048 -> h_Vptr x_4048
     110| Vptr x_2487 -> h_Vptr x_2487
    115111
    116112(** val val_rect_Type2 :
     
    119115let rec val_rect_Type2 h_Vundef h_Vint h_Vnull h_Vptr = function
    120116| Vundef -> h_Vundef
    121 | Vint (sz, x_4054) -> h_Vint sz x_4054
     117| Vint (sz, x_2493) -> h_Vint sz x_2493
    122118| Vnull -> h_Vnull
    123 | Vptr x_4055 -> h_Vptr x_4055
     119| Vptr x_2494 -> h_Vptr x_2494
    124120
    125121(** val val_rect_Type1 :
     
    128124let rec val_rect_Type1 h_Vundef h_Vint h_Vnull h_Vptr = function
    129125| Vundef -> h_Vundef
    130 | Vint (sz, x_4061) -> h_Vint sz x_4061
     126| Vint (sz, x_2500) -> h_Vint sz x_2500
    131127| Vnull -> h_Vnull
    132 | Vptr x_4062 -> h_Vptr x_4062
     128| Vptr x_2501 -> h_Vptr x_2501
    133129
    134130(** val val_rect_Type0 :
     
    137133let rec val_rect_Type0 h_Vundef h_Vint h_Vnull h_Vptr = function
    138134| Vundef -> h_Vundef
    139 | Vint (sz, x_4068) -> h_Vint sz x_4068
     135| Vint (sz, x_2507) -> h_Vint sz x_2507
    140136| Vnull -> h_Vnull
    141 | Vptr x_4069 -> h_Vptr x_4069
     137| Vptr x_2508 -> h_Vptr x_2508
    142138
    143139(** val val_inv_rect_Type4 :
     
    218214| Bool.False -> vfalse
    219215
    220 (** val valueNotABoolean : String.string **)
    221 let valueNotABoolean = "value not a boolean"
    222   (*failwith "AXIOM TO BE REALIZED"*)
    223 
    224216(** val eval_bool_of_val : val0 -> Bool.bool Errors.res **)
    225217let eval_bool_of_val = function
    226 | Vundef -> Errors.Error (Errors.msg valueNotABoolean)
     218| Vundef -> Errors.Error (Errors.msg ErrorMessages.ValueNotABoolean)
    227219| Vint (x, i) ->
    228220  Errors.OK
Note: See TracChangeset for help on using the changeset viewer.