diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2018-06-15 12:53:01 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2018-06-17 11:38:47 +0200 |
| commit | abd89e37c2882e0f92a3e119b4eb7ee44cc8a503 (patch) | |
| tree | 6432e7b5e0fad15dddcd7aeda86ba199c15d0557 /pretyping | |
| parent | d62354b7e9ff8e20aa959984b392a27e26f9fc24 (diff) | |
Fixes #7811 (uncaught Not_found in notation printer related to "match").
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/glob_ops.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml index 8ecec30cf..11cfd2040 100644 --- a/pretyping/glob_ops.ml +++ b/pretyping/glob_ops.ml @@ -414,8 +414,10 @@ let loc_of_glob_constr c = c.CAst.loc (**********************************************************************) (* Alpha-renaming *) +exception UnsoundRenaming + let collide_id l id = List.exists (fun (id',id'') -> Id.equal id id' || Id.equal id id'') l -let test_id l id = if collide_id l id then raise Not_found +let test_id l id = if collide_id l id then raise UnsoundRenaming let test_na l na = Name.iter (test_id l) na let update_subst na l = @@ -429,8 +431,6 @@ let update_subst na l = else na,l) na (na,l) -exception UnsoundRenaming - let rename_var l id = try let id' = Id.List.assoc id l in |