diff options
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 c2b27ca6a..dcc6ef88b 100644 --- a/pretyping/glob_ops.mli +++ b/pretyping/glob_ops.mli @@ -44,6 +44,8 @@ val bound_glob_vars : glob_constr -> Id.Set.t val loc_of_glob_constr : glob_constr -> Loc.t val glob_visible_short_qualid : glob_constr -> Id.t list +val rename_glob_vars : (Id.t * Id.t) list -> glob_constr -> glob_constr + (** [map_pattern_binders f m c] applies [f] to all the binding names in a pattern-matching expression ({!Glob_term.GCases}) represented here by its relevant components [m] and [c]. It is used to |