diff options
| author | msozeau | 2008-06-06 22:39:43 +0000 |
|---|---|---|
| committer | msozeau | 2008-06-06 22:39:43 +0000 |
| commit | a1fe45ddbd37d3c447a23cde0ee21f105ef42ac0 (patch) | |
| tree | 648a977d3137ffa9c7cc97e8503c0a5d8620dbfa /library/library.ml | |
| parent | 0cdfa2fb137989f75cdebfa3a64726bc0d56a8af (diff) | |
Enhancements to coqdoc, better globalization of sections and modules.
Minor fix in Morphisms which prevented working with higher-order
morphisms and PER relations.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11065 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'library/library.ml')
| -rw-r--r-- | library/library.ml | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/library/library.ml b/library/library.ml index e53c0cd1a1..c014865fe5 100644 --- a/library/library.ml +++ b/library/library.ml @@ -536,6 +536,10 @@ let require_library qidl export = end else add_anonymous_leaf (in_require (needed,modrefl,export)); + if !Flags.dump then List.iter2 (fun (loc, _) dp -> + Flags.dump_string (Printf.sprintf "R%d %s <> <> %s\n" + (fst (unloc loc)) (string_of_dirpath dp) "lib")) + qidl modrefl; if !Flags.xml_export then List.iter !xml_require modrefl; add_frozen_state () |