From 582b5147cb79267ce79c03718cb3575826dc831c Mon Sep 17 00:00:00 2001
From: notin
Date: Tue, 23 May 2006 17:52:43 +0000
Subject: Modification de add_glob (support des modules dans Coqdoc)

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

(limited to 'kernel')

diff --git a/kernel/names.ml b/kernel/names.ml
index 7b83e18c3a..d73af7fa1d 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -198,6 +198,10 @@ let con_label = label
 let pr_con = pr_kn
 let con_modpath = modpath
 
+let mind_modpath = modpath
+let ind_modpath ind = mind_modpath (fst ind)
+let constr_modpath c = ind_modpath (fst c)
+
 let ith_mutual_inductive (kn,_) i = (kn,i)
 let ith_constructor_of_inductive ind i = (ind,i)
 let inductive_of_constructor (ind,i) = ind
diff --git a/kernel/names.mli b/kernel/names.mli
index 0e65b65b40..4c51269d08 100644
--- a/kernel/names.mli
+++ b/kernel/names.mli
@@ -134,6 +134,10 @@ val con_label : constant -> label
 val con_modpath : constant -> module_path
 val pr_con : constant -> Pp.std_ppcmds
 
+val mind_modpath : mutual_inductive -> module_path
+val ind_modpath : inductive -> module_path
+val constr_modpath : constructor -> module_path
+
 val ith_mutual_inductive : inductive -> int -> inductive
 val ith_constructor_of_inductive : inductive -> int -> constructor
 val inductive_of_constructor : constructor -> inductive
-- 
cgit v1.2.3