From 7208928de37565a9e38f9540f2bfb1e7a3b877e6 Mon Sep 17 00:00:00 2001
From: ppedrot
Date: Mon, 17 Sep 2012 20:46:20 +0000
Subject: More cleaning on Utils and CList. Some parts of the code being
 peculiarly messy, I hope I did not introduce too many bugs.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15815 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 library/nameops.ml  | 2 +-
 library/nameops.mli | 2 ++
 2 files changed, 3 insertions(+), 1 deletion(-)

(limited to 'library')

diff --git a/library/nameops.ml b/library/nameops.ml
index 01a9a62403..5ea7e26855 100644
--- a/library/nameops.ml
+++ b/library/nameops.ml
@@ -114,7 +114,7 @@ let atompart_of_id id = fst (repr_ident id)
 
 let out_name = function
   | Name id -> id
-  | Anonymous -> failwith "out_name: expects a defined name"
+  | Anonymous -> failwith "Nameops.out_name"
 
 let name_fold f na a =
   match na with
diff --git a/library/nameops.mli b/library/nameops.mli
index c90aa7c782..fb26c1910d 100644
--- a/library/nameops.mli
+++ b/library/nameops.mli
@@ -26,6 +26,8 @@ val lift_subscript   : identifier -> identifier
 val forget_subscript : identifier -> identifier
 
 val out_name : name -> identifier
+(** [out_name] associates [id] to [Name id]. Raises [Failure "Nameops.out_name"]
+    otherwise. *)
 
 val name_fold : (identifier -> 'a -> 'a) -> name -> 'a -> 'a
 val name_iter : (identifier -> unit) -> name -> unit
-- 
cgit v1.2.3