From f0059e376230a40567374d4a00875ff00a6e6cc7 Mon Sep 17 00:00:00 2001
From: sacerdot
Date: Fri, 26 Mar 2004 21:08:31 +0000
Subject: Theory file for file A.B.C.v is put in A/B/C.theory.xml. It was put
 in file A/B/C/C.theory.xml.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5581 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 contrib/xml/xmlcommand.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'contrib/xml/xmlcommand.ml')

diff --git a/contrib/xml/xmlcommand.ml b/contrib/xml/xmlcommand.ml
index da977a18b9..3cb16a97a6 100644
--- a/contrib/xml/xmlcommand.ml
+++ b/contrib/xml/xmlcommand.ml
@@ -227,8 +227,8 @@ let theory_filename xml_library_root =
   | Some xml_library_root' ->
      let toks = List.map N.string_of_id (N.repr_dirpath (Lib.library_dp ())) in
      let hd = List.hd toks in
-     (* theory from A/B/C/F.v goes into A/B/C/F/F.theory *)
-     let alltoks = List.rev (hd :: toks) in
+     (* theory from A/B/C/F.v goes into A/B/C/F.theory *)
+     let alltoks = List.rev toks in
        Some (join_dirs xml_library_root' alltoks ^ ".theory")
 
 let print_object uri obj sigma proof_tree_infos filename =
-- 
cgit v1.2.3