aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping')
-rw-r--r--pretyping/glob_ops.ml6
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