diff options
| author | Gaëtan Gilbert | 2019-03-17 10:40:31 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-03-18 12:52:42 +0100 |
| commit | a71f586e23b0e68032c556bfa1c37df8f4358c71 (patch) | |
| tree | 876772675b8bcf7cfa3d4ff2b7ea460c62ebd04f /pretyping/glob_ops.mli | |
| parent | 9ac5483132b42e845a0708491843693b70893eef (diff) | |
Fix constr_matching on SProp
Diffstat (limited to 'pretyping/glob_ops.mli')
| -rw-r--r-- | pretyping/glob_ops.mli | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/pretyping/glob_ops.mli b/pretyping/glob_ops.mli index c189a3bcb2..2f0ac76235 100644 --- a/pretyping/glob_ops.mli +++ b/pretyping/glob_ops.mli @@ -15,6 +15,8 @@ open Glob_term val glob_sort_eq : Glob_term.glob_sort -> Glob_term.glob_sort -> bool +val glob_sort_family : 'a glob_sort_gen -> Sorts.family + val cases_pattern_eq : 'a cases_pattern_g -> 'a cases_pattern_g -> bool val alias_of_pat : 'a cases_pattern_g -> Name.t |