diff options
| author | filliatr | 2002-02-14 14:39:07 +0000 |
|---|---|---|
| committer | filliatr | 2002-02-14 14:39:07 +0000 |
| commit | 67f72c93f5f364591224a86c52727867e02a8f71 (patch) | |
| tree | ecf630daf8346e77e6620233d8f3e6c18a0c9b3c /library | |
| parent | b239b208eb9a66037b0c629cf7ccb6e4b110636a (diff) | |
option -dump-glob pour coqdoc
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2474 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'library')
| -rw-r--r-- | library/declare.ml | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/library/declare.ml b/library/declare.ml index 9741ca9fa5..1bd7ad97e1 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -390,7 +390,8 @@ let library_part ref = let sp = Nametab.sp_of_global (Global.env ()) ref in let dir,_ = repr_path sp in match strength_of_global ref with - | DischargeAt (dp,n) -> extract_dirpath_prefix n dp + | DischargeAt (dp,n) -> + extract_dirpath_prefix n dp | NeverDischarge -> if is_dirpath_prefix_of dir (Lib.cwd ()) then (* Theorem/Lemma not yet (fully) discharged *) @@ -399,5 +400,3 @@ let library_part ref = (* Theorem/Lemma outside its outer section of definition *) dir | NotDeclare -> assert false - - |