diff options
Diffstat (limited to 'pretyping/glob_ops.mli')
| -rw-r--r-- | pretyping/glob_ops.mli | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/pretyping/glob_ops.mli b/pretyping/glob_ops.mli index 67f3cb41..e514fd52 100644 --- a/pretyping/glob_ops.mli +++ b/pretyping/glob_ops.mli @@ -13,6 +13,9 @@ open Glob_term val cases_pattern_eq : cases_pattern -> cases_pattern -> bool +val cast_type_eq : ('a -> 'a -> bool) -> + 'a Misctypes.cast_type -> 'a Misctypes.cast_type -> bool + val glob_constr_eq : glob_constr -> glob_constr -> bool (** Operations on [glob_constr] *) |