From a3f82d0d498a81612618f39481ed829e857afd3c Mon Sep 17 00:00:00 2001
From: letouzey
Date: Fri, 15 Mar 2013 18:47:11 +0000
Subject: Extract_env : correct exceptions mentionned in a try ... with

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16306 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 interp/smartlocate.mli            | 9 ++++++---
 plugins/extraction/extract_env.ml | 2 +-
 2 files changed, 7 insertions(+), 4 deletions(-)

diff --git a/interp/smartlocate.mli b/interp/smartlocate.mli
index e1bb3459a0..5f772c5915 100644
--- a/interp/smartlocate.mli
+++ b/interp/smartlocate.mli
@@ -14,8 +14,8 @@ open Globnames
 open Misctypes
 
 (** [locate_global_with_alias] locates global reference possibly following
-   a notation if this notation has a role of aliasing; raise Not_found
-   if not bound in the global env; raise an error if bound to a
+   a notation if this notation has a role of aliasing; raise [Not_found]
+   if not bound in the global env; raise a [UserError] if bound to a
    syntactic def that does not denote a reference *)
 
 val locate_global_with_alias : qualid located -> global_reference
@@ -23,7 +23,10 @@ val locate_global_with_alias : qualid located -> global_reference
 (** Extract a global_reference from a reference that can be an "alias" *)
 val global_of_extended_global : extended_global_reference -> global_reference
 
-(** Locate a reference taking into account possible "alias" notations *)
+(** Locate a reference taking into account possible "alias" notations.
+    May raise [Nametab.GlobalizationError _] for an unknown reference,
+    or a [UserError] if bound to a syntactic def that does not denote
+    a reference. *)
 val global_with_alias : reference -> global_reference
 
 (** The same for inductive types *)
diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml
index a64cc3d705..add5428b5c 100644
--- a/plugins/extraction/extract_env.ml
+++ b/plugins/extraction/extract_env.ml
@@ -545,7 +545,7 @@ let rec locate_ref = function
       let mpo = try Some (Nametab.locate_module q) with Not_found -> None
       and ro =
         try Some (Smartlocate.global_with_alias r)
-        with Not_found | UserError _ -> None
+        with Nametab.GlobalizationError _ | UserError _ -> None
       in
       match mpo, ro with
 	| None, None -> Nametab.error_global_not_found q
-- 
cgit v1.2.3