From 2c6002d1fbf08ee68914227e3a4267cb38ff8b81 Mon Sep 17 00:00:00 2001 From: filliatr Date: Fri, 10 Sep 1999 14:00:56 +0000 Subject: modules System, Lib et States git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@71 85f007b7-540e-0410-9357-904b9bb8a0f7 --- kernel/names.ml | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) (limited to 'kernel/names.ml') 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 } -- cgit v1.2.3