aboutsummaryrefslogtreecommitdiffhomepage
path: root/checker/term.mli
diff options
context:
space:
mode:
Diffstat (limited to 'checker/term.mli')
-rw-r--r--checker/term.mli2
1 files changed, 1 insertions, 1 deletions
diff --git a/checker/term.mli b/checker/term.mli
index c417cd14e..cc9d5cf97 100644
--- a/checker/term.mli
+++ b/checker/term.mli
@@ -23,7 +23,7 @@ type 'a pexistential = existential_key * 'a array
type 'a prec_declaration = name array * 'a array * 'a array
type 'a pfixpoint = (int array * int) * 'a prec_declaration
type 'a pcofixpoint = int * 'a prec_declaration
-type cast_kind = VMcast | DEFAULTcast
+type cast_kind = VMcast | NATIVEcast | DEFAULTcast
type constr =
Rel of int
| Var of Id.t