diff options
Diffstat (limited to 'intf/misctypes.mli')
| -rw-r--r-- | intf/misctypes.mli | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/intf/misctypes.mli b/intf/misctypes.mli index 3a044018c4..164fd60c9e 100644 --- a/intf/misctypes.mli +++ b/intf/misctypes.mli @@ -58,6 +58,7 @@ type 'a cast_type = | CastConv of 'a | CastVM of 'a | CastCoerce (** Cast to a base type (eg, an underlying inductive type) *) + | CastNative of 'a (** Bindings *) |