diverses fonctions ajoutees

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@170 85f007b7-540e-0410-9357-904b9bb8a0f7

4 files changed, 8 insertions, 0 deletions

diff --git a/kernel/names.ml b/kernel/names.ml
index dc1350fa39..316e0735a9 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -198,6 +198,10 @@ let append_to_path sp str =
   let (sp,id,k) = repr_path sp in
   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"
+
 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 9a7822d117..541e4f61a6 100644
--- a/kernel/names.mli
+++ b/kernel/names.mli
@@ -49,6 +49,8 @@ val dirpath : section_path -> string list
 val basename : section_path -> identifier
 val kind_of_path : section_path -> path_kind
 
+val sp_of_wd : string list -> section_path
+
 val path_of_string : string -> section_path
 val string_of_path : section_path -> string
 val string_of_path_mind : section_path -> identifier -> string
diff --git a/kernel/term.ml b/kernel/term.ml
index 91061c7ca3..1a5c74e682 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -69,6 +69,7 @@ let make_typed t s = { body = t; typ = s }
 let typed_app f tt = { body = f tt.body; typ = tt.typ }
 
 let body_of_type ty = ty.body
+let level_of_type t = (t.typ : sorts)
 
 let incast_type tty = DOP2 (Cast, tty.body, (DOP0 (Sort tty.typ)))
 
diff --git a/kernel/term.mli b/kernel/term.mli
index b04248a040..b849258606 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -59,6 +59,7 @@ val make_typed : constr -> sorts -> typed_type
 val typed_app : (constr -> constr) -> typed_type -> typed_type
 
 val body_of_type : typed_type -> constr
+val level_of_type : typed_type -> sorts
 
 val incast_type : typed_type -> constr