diff options
| author |  Arnaud Spiwack <arnaud@spiwack.net> | 2014-11-14 09:40:23 +0100 |
|---|---|---|
| committer | Arnaud Spiwack <arnaud@spiwack.net> | 2014-11-19 10:11:45 +0100 |
| commit | bd2dd62ea83ff9374bd28f089b19d3abba6ac7cb (patch) | |
| tree | 9be4b23ec2ae2f6d83c1d1d45eedf0bfe74611d3 /pretyping/glob_ops.mli | |
| parent | 9e1224f452470c3e18e13c88c4d8a00fe0864c16 (diff) | |
Glob-ops: a name-mapping operation for pattern-matching binders.
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 9e0aac909..41d1d51a5 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, |