diff options
author | 2005-01-31 14:34:14 +0000 | |
---|---|---|
committer | 2005-01-31 14:34:14 +0000 | |
commit | e669490d0d5e6ed4bb45c895194791f01d038637 (patch) | |
tree | 4eb40b447e6573dbaa1cf593a2cae6758850cb7c /library/lib.ml | |
parent | d334716fb2d09dd3304f98ee0dbf39275eac010b (diff) | |
parent | 6497f27021fec4e01f2182014f2bb1989b4707f9 (diff) |
Merge commit 'upstream/8.0pl2'
Diffstat (limited to 'library/lib.ml')
-rw-r--r-- | library/lib.ml | 14 |
1 files changed, 13 insertions, 1 deletions
diff --git a/library/lib.ml b/library/lib.ml index b9da6dea..a9f864ef 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: lib.ml,v 1.63.2.2 2004/07/16 19:30:35 herbelin Exp $ *) +(* $Id: lib.ml,v 1.63.2.3 2004/11/22 14:21:23 herbelin Exp $ *) open Pp open Util @@ -564,3 +564,15 @@ let library_part ref = else (* Theorem/Lemma outside its outer section of definition *) dir + + +let rec file_of_mp = function + | MPfile dir -> Some dir + | MPself _ -> Some (library_dp ()) + | MPbound _ -> None + | MPdot (mp,_) -> file_of_mp mp + +let file_part = function + | VarRef id -> anomaly "TODO"; + | ConstRef kn | ConstructRef ((kn,_),_) | IndRef (kn,_) -> + file_of_mp (modpath kn) |