diff options
Diffstat (limited to 'pretyping/glob_ops.ml')
| -rw-r--r-- | pretyping/glob_ops.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml index 8ecec30cf..ba193da60 100644 --- a/pretyping/glob_ops.ml +++ b/pretyping/glob_ops.ml @@ -51,7 +51,7 @@ let glob_sort_eq g1 g2 = let open Glob_term in match g1, g2 with | GProp, GProp -> true | GSet, GSet -> true | GType l1, GType l2 -> - List.equal (Option.equal (fun (x,m) (y,n) -> Libnames.eq_reference x y && Int.equal m n)) l1 l2 + List.equal (Option.equal (fun (x,m) (y,n) -> Libnames.qualid_eq x y && Int.equal m n)) l1 l2 | _ -> false let binding_kind_eq bk1 bk2 = match bk1, bk2 with @@ -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 |