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 ++++++---
 1 file changed, 6 insertions(+), 3 deletions(-)

(limited to 'interp')

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