diff options
Diffstat (limited to 'pretyping/glob_ops.mli')
| -rw-r--r-- | pretyping/glob_ops.mli | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/pretyping/glob_ops.mli b/pretyping/glob_ops.mli index 9e0aac909f..41d1d51a54 100644 --- a/pretyping/glob_ops.mli +++ b/pretyping/glob_ops.mli @@ -37,6 +37,14 @@ val occur_glob_constr : Id.t -> glob_constr -> bool val free_glob_vars : glob_constr -> Id.t list val loc_of_glob_constr : glob_constr -> Loc.t +(** [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 + interpret Ltac-bound names both in pretyping and printing of + terms. *) +val map_pattern_binders : (name -> name) -> + tomatch_tuples -> cases_clauses -> (tomatch_tuples*cases_clauses) + (** Conversion from glob_constr to cases pattern, if possible Take the current alias as parameter, |