diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-07-18 15:09:08 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-07-18 15:51:02 +0200 |
| commit | fd0cd480a720cbba15de86bbc9cad74ba6d89675 (patch) | |
| tree | 157da3e6f8a88f752fe516e34d70d58a7864021c /pretyping/glob_ops.mli | |
| parent | 2042daa9a6e13cbb9636a62812015749d95c2283 (diff) | |
A new step on using alpha-conversion in printing notations.
A couple of bugs have been found.
Example #4932 is now printing correctly in the presence of multiple
binders (when no let-in, no irrefutable patterns).
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 dcc6ef88b..55e6b6533 100644 --- a/pretyping/glob_ops.mli +++ b/pretyping/glob_ops.mli @@ -44,6 +44,14 @@ 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 +(* Renaming free variables using a renaming map; fails with + [UnsoundRenaming] if applying the renaming would introduce + collision, as in, e.g., renaming [P x y] using substitution [(x,y)]; + inner alpha-conversion done only for forall, fun, let but + not for cases and fix *) + +exception UnsoundRenaming +val rename_var : (Id.t * Id.t) list -> Id.t -> Id.t 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 |