From 162fc39bcc36953402d668b5d7ac7b88c9966461 Mon Sep 17 00:00:00 2001
From: filliatr
Date: Thu, 2 Dec 1999 16:43:08 +0000
Subject: modifs pour premiere edition de liens

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

(limited to 'kernel')

diff --git a/kernel/evd.ml b/kernel/evd.ml
index cc95958bc9..6853fc9c46 100644
--- a/kernel/evd.ml
+++ b/kernel/evd.ml
@@ -23,7 +23,7 @@ type 'a evar_info = {
   evar_concl : constr;
   evar_env : env;
   evar_body : evar_body;
-  evar_info : 'a }
+  evar_info : 'a option }
 
 type 'a evar_map = 'a evar_info Intmap.t
 
diff --git a/kernel/evd.mli b/kernel/evd.mli
index 1b00cddb4a..e9f7818ffa 100644
--- a/kernel/evd.mli
+++ b/kernel/evd.mli
@@ -26,7 +26,7 @@ type 'a evar_info = {
   evar_concl : constr;
   evar_env : env;
   evar_body : evar_body;
-  evar_info : 'a }
+  evar_info : 'a option }
 
 type 'a evar_map
 
diff --git a/kernel/names.ml b/kernel/names.ml
index e04a41f42b..dd7ad6f3a6 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -202,6 +202,9 @@ let sp_of_wd = function
   | bn::dp -> make_path dp (id_of_string bn) OBJ
   | _      -> invalid_arg "Names.sp_of_wd"
 
+let wd_of_sp sp = 
+  let (sp,id,_) = repr_path sp in sp @ [string_of_id id]
+
 let sp_ord sp1 sp2 =
   let (p1,id1,k) = repr_path sp1
   and (p2,id2,k') = repr_path sp2 in
diff --git a/kernel/names.mli b/kernel/names.mli
index b3f5811e4c..1ccf3c12ce 100644
--- a/kernel/names.mli
+++ b/kernel/names.mli
@@ -50,6 +50,7 @@ val basename : section_path -> identifier
 val kind_of_path : section_path -> path_kind
 
 val sp_of_wd : string list -> section_path
+val wd_of_sp : section_path -> string list
 
 val path_of_string : string -> section_path
 val string_of_path : section_path -> string
-- 
cgit v1.2.3