From 4a2b9073e61de1ab000b26652d94e63b382ce7d2 Mon Sep 17 00:00:00 2001
From: filliatr
Date: Fri, 3 Dec 1999 16:23:22 +0000
Subject: bug make_strength repare

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@200 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 kernel/names.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'kernel')

diff --git a/kernel/names.ml b/kernel/names.ml
index dd7ad6f3a6..2686763aa6 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -199,8 +199,8 @@ let append_to_path sp str =
   make_path sp (id_of_string ((string_of_id id)^str)) k
 
 let sp_of_wd = function
-  | bn::dp -> make_path dp (id_of_string bn) OBJ
-  | _      -> invalid_arg "Names.sp_of_wd"
+  | [] -> invalid_arg "Names.sp_of_wd"
+  | l -> let (bn,dp) = list_sep_last l in make_path dp (id_of_string bn) OBJ
 
 let wd_of_sp sp = 
   let (sp,id,_) = repr_path sp in sp @ [string_of_id id]
-- 
cgit v1.2.3