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 467b72e520..37aa31d094 100644 --- a/pretyping/glob_ops.mli +++ b/pretyping/glob_ops.mli @@ -48,6 +48,9 @@ val mkGApp : ?loc:Loc.t -> 'a glob_constr_g -> 'a glob_constr_g -> 'a glob_const val map_glob_constr : (glob_constr -> glob_constr) -> glob_constr -> glob_constr +(** Equality on [binding_kind] *) +val binding_kind_eq : binding_kind -> binding_kind -> bool + (** Ensure traversal from left to right *) val map_glob_constr_left_to_right : (glob_constr -> glob_constr) -> glob_constr -> glob_constr |