From abd89e37c2882e0f92a3e119b4eb7ee44cc8a503 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin <Hugo.Herbelin@inria.fr>
Date: Fri, 15 Jun 2018 12:53:01 +0200
Subject: Fixes #7811 (uncaught Not_found in notation printer related to
 "match").

---
 pretyping/glob_ops.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'pretyping')

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
-- 
cgit v1.2.3