diff options
Diffstat (limited to 'pretyping/glob_term.ml')
| -rw-r--r-- | pretyping/glob_term.ml | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/pretyping/glob_term.ml b/pretyping/glob_term.ml index 9f93e5e6c1..d480c12834 100644 --- a/pretyping/glob_term.ml +++ b/pretyping/glob_term.ml @@ -57,7 +57,6 @@ and glob_fix_kind = type 'a cast_type = | CastConv of 'a | CastVM of 'a - | CastCoerce (** Cast to a base type (eg, an underlying inductive type) *) | CastNative of 'a (** The kind of patterns that occurs in "match ... with ... end" |