aboutsummaryrefslogtreecommitdiffhomepage
path: root/library
diff options
context:
space:
mode:
authorGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2013-03-13 00:00:08 +0000
committerGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2013-03-13 00:00:08 +0000
commitda3cbbcef1f4de9780603225e095f026bb5da709 (patch)
tree245855016cea9d25fcd643f841bc868bd81ec440 /library
parent108e88cafee662932c99a83230f674f648866613 (diff)
Restrict (try...with...) to avoid catching critical exn (part 6)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16282 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'library')
-rw-r--r--library/nametab.mli6
1 files changed, 4 insertions, 2 deletions
diff --git a/library/nametab.mli b/library/nametab.mli
index d561735fd..43c174f1b 100644
--- a/library/nametab.mli
+++ b/library/nametab.mli
@@ -151,13 +151,15 @@ val path_of_tactic : ltac_constant -> full_path
val dirpath_of_global : global_reference -> DirPath.t
val basename_of_global : global_reference -> Id.t
-(** Printing of global references using names as short as possible *)
+(** Printing of global references using names as short as possible.
+ @raise Not_found when the reference is not in the global tables. *)
val pr_global_env : Id.Set.t -> global_reference -> std_ppcmds
(** The [shortest_qualid] functions given an object with [user_name]
Coq.A.B.x, try to find the shortest among x, B.x, A.B.x and
- Coq.A.B.x that denotes the same object. *)
+ Coq.A.B.x that denotes the same object.
+ @raise Not_found for unknown objects. *)
val shortest_qualid_of_global : Id.Set.t -> global_reference -> qualid
val shortest_qualid_of_syndef : Id.Set.t -> syndef_name -> qualid