diff options
Diffstat (limited to 'checker/values.mli')
| -rw-r--r-- | checker/values.mli | 19 |
1 files changed, 19 insertions, 0 deletions
diff --git a/checker/values.mli b/checker/values.mli index 1b1437a469..616b69907f 100644 --- a/checker/values.mli +++ b/checker/values.mli @@ -10,17 +10,36 @@ type value = | Any + (** A value that we won't check, *) + | Fail of string + (** A value that shouldn't be there at all, *) + | Tuple of string * value array + (** A debug name and sub-values in this block *) + | 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 *) + | Array of value | List of value | Opt of value | Int | String + (** Builtin Ocaml types. *) + | Annot of string * value + (** Adds a debug note to the inner value *) + | Dyn + (** Coq's Dyn.t *) + | Proxy of value ref + (** Same as the inner value, used to define recursive types *) + +(** NB: List and Opt have their own constructors to make it easy to + define eg [let rec foo = List foo]. *) val v_univopaques : value val v_libsum : value |