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

...

File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/typeComparison.ml

    r2601 r2649  
    33open CostLabel
    44
     5open Coqlib
     6
    57open Proper
    68
     
    911open Deqsets
    1012
     13open ErrorMessages
     14
    1115open PreIdentifiers
    1216
     
    2731open Identifiers
    2832
    29 open Coqlib
    30 
    31 open Floats
    32 
    3333open Arithmetic
    3434
    35 open Char
    36 
    37 open String
    38 
    3935open Vector
    4036
     
    7672
    7773open Csyntax
    78 
    79 (** val typeMismatch : String.string **)
    80 let typeMismatch = "type mismatch"
    81   (*failwith "AXIOM TO BE REALIZED"*)
    8274
    8375(** val sz_eq_dec : AST.intsize -> AST.intsize -> (__, __) Types.sum **)
     
    280272  match type_eq_dec t1 t2 with
    281273  | Types.Inl _ -> Errors.OK __
    282   | Types.Inr _ -> Errors.Error (Errors.msg typeMismatch)
     274  | Types.Inr _ -> Errors.Error (Errors.msg ErrorMessages.TypeMismatch)
    283275
    284276(** val type_eq : Csyntax.type0 -> Csyntax.type0 -> Bool.bool **)
Note: See TracChangeset for help on using the changeset viewer.