From 305ccf3523bf356c9e099f2f0c848bfba4b61e94 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Mon, 2 Mar 2020 03:18:23 -0500
Subject: [vernac] Make local exception local

---
 vernac/vernacentries.ml | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index f935cea534..151e675e8c 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -1603,12 +1603,11 @@ let get_nth_goal ~pstate n =
   let gl = {Evd.it=List.nth goals (n-1) ; sigma = sigma; } in
   gl
 
-exception NoHyp
-
 (* Printing "About" information of a hypothesis of the current goal.
    We only print the type and a small statement to this comes from the
    goal. Precondition: there must be at least one current goal. *)
 let print_about_hyp_globs ~pstate ?loc ref_or_by_not udecl glopt =
+  let exception NoHyp in
   let open Context.Named.Declaration in
   try
     (* Fallback early to globals *)
-- 
cgit v1.2.3