aboutsummaryrefslogtreecommitdiff
path: root/kernel/names.ml
diff options
context:
space:
mode:
authorfilliatr1999-09-10 14:00:56 +0000
committerfilliatr1999-09-10 14:00:56 +0000
commit2c6002d1fbf08ee68914227e3a4267cb38ff8b81 (patch)
tree83caeab0f53e7b4fc72ffb1637a0696f0231a2ed /kernel/names.ml
parent540bd2b46fd848fbf6d1f8c2804580d3afed98a6 (diff)
modules System, Lib et States
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@71 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/names.ml')
-rw-r--r--kernel/names.ml4
1 files changed, 3 insertions, 1 deletions
diff --git a/kernel/names.ml b/kernel/names.ml
index af07ba426f..6e5835fbb1 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -55,7 +55,7 @@ let print_id { atom = a; index = n } =
| ("",n) -> [< 'sTR"[" ; 'iNT n ; 'sTR"]" >]
| (s,n) -> [< 'sTR s ; (if n = (-1) then [< >] else [< 'iNT n >]) >]
-let pr_idl idl = prlist_with_sep pr_spc print_id idl
+let print_idl idl = prlist_with_sep pr_spc print_id idl
let id_ord id1 id2 =
let (s1,n1) = repr_ident id1
@@ -168,6 +168,8 @@ let path_of_string s =
with
| Invalid_argument _ -> invalid_arg "path_of_string"
+let print_sp sp = [< 'sTR (string_of_path sp) >]
+
let coerce_path k { dirpath = p; basename = id } =
{ dirpath = p; basename = id; kind = k }