Module Coq_checklib.ValuesSource

Sourcetype value =
  1. | Any
    (*

    A value that we won't check,

    *)
  2. | Fail of string
    (*

    A value that shouldn't be there at all,

    *)
  3. | Tuple of string * value array
    (*

    A debug name and sub-values in this block

    *)
  4. | Sum of string * int * value array array
    (*

    A debug name, a number of constant constructors, and sub-values at each position of each possible constructed variant

    *)
  5. | Array of value
  6. | List of value
  7. | Opt of value
  8. | Int
  9. | String
    (*

    Builtin Ocaml types.

    *)
  10. | Annot of string * value
    (*

    Adds a debug note to the inner value

    *)
  11. | Dyn
    (*

    Coq's Dyn.t

    *)
  12. | Proxy of value ref
    (*

    Same as the inner value, used to define recursive types

    *)
  13. | Int64
  14. | Float64

NB: List and Opt have their own constructors to make it easy to define eg let rec foo = List foo.

Sourceval v_univopaques : value
Sourceval v_libsum : value
Sourceval v_lib : value
Sourceval v_opaquetable : value
Sourceval v_stm_seg : value
Sourceval v_vmlib : value