diff options
Diffstat (limited to 'pretyping/miscops.mli')
| -rw-r--r-- | pretyping/miscops.mli | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/pretyping/miscops.mli b/pretyping/miscops.mli index 84541a3b2..6235533d7 100644 --- a/pretyping/miscops.mli +++ b/pretyping/miscops.mli @@ -16,3 +16,8 @@ val smartmap_cast_type : ('a -> 'a) -> 'a cast_type -> 'a cast_type (** Equalities on [glob_sort] *) val glob_sort_eq : glob_sort -> glob_sort -> bool + +(** Equalities on [intro_pattern_naming] *) + +val intro_pattern_naming_eq : + intro_pattern_naming_expr -> intro_pattern_naming_expr -> bool |