diff options
Diffstat (limited to 'pretyping/glob_ops.mli')
| -rw-r--r-- | pretyping/glob_ops.mli | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/pretyping/glob_ops.mli b/pretyping/glob_ops.mli index 5195b98c8..1785c87be 100644 --- a/pretyping/glob_ops.mli +++ b/pretyping/glob_ops.mli @@ -18,7 +18,6 @@ open Locus open Glob_term (** Equalities *) -val glob_sort_eq : glob_sort -> glob_sort -> bool val cases_pattern_eq : cases_pattern -> cases_pattern -> bool |