diff options
| author | Pierre-Marie Pédrot | 2015-03-24 16:01:03 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2015-03-24 16:50:59 +0100 |
| commit | 7c044bd9b5bca4970f6a936d5b6d5484bcb79397 (patch) | |
| tree | 280cfc3f316502cf6b4249f4cafe8c8c871d748c /pretyping/glob_ops.mli | |
| parent | d65eaaaa8cb311a0344a584df7a4b405034780b9 (diff) | |
Fixing equality of notation_constrs. Fixes bug #4136.
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 67f3cb4169..e514fd529e 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] *) |