section_path etait en fait bonne dans ast et buggee dans printer.ml

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1074 85f007b7-540e-0410-9357-904b9bb8a0f7

2 files changed, 5 insertions, 9 deletions

diff --git a/parsing/ast.ml b/parsing/ast.ml
index f541d77a6..22db3cdfd 100755
--- a/parsing/ast.ml
+++ b/parsing/ast.ml
@@ -44,12 +44,11 @@ let rec set_loc loc = function
 
 let path_section loc sp =
   let (sl,bn,pk) = repr_path sp in
-  Coqast.Path(loc, string_of_id bn :: (List.rev sl), string_of_kind pk)
+  Coqast.Path(loc, sl @ [string_of_id bn], string_of_kind pk)
 
 let section_path sl k =
-  match sl with
-    | s::pa -> 
-	make_path (List.rev pa) (id_of_string s) (kind_of_string k)
+  match List.rev sl with
+    | s::pa -> make_path (List.rev pa) (id_of_string s) (kind_of_string k)
     | [] -> invalid_arg "section_path"
 
 (* ast destructors *)
diff --git a/parsing/printer.ml b/parsing/printer.ml
index 25578ad76..5169b8d3b 100644
--- a/parsing/printer.ml
+++ b/parsing/printer.ml
@@ -10,15 +10,12 @@ open Environ
 open Global
 open Declare
 open Coqast
+open Ast
 open Termast
 
 let emacs_str s = if !Options.print_emacs then s else "" 
 
-let dfltpr ast = [< 'sTR"#GENTERM " ; Ast.print_ast ast >];;
-
-let section_path sl s =
-  let sl = List.rev sl in
-  make_path (List.tl sl) (id_of_string (List.hd sl)) (kind_of_string s)
+let dfltpr ast = [< 'sTR"#GENTERM " ; print_ast ast >];;
 
 let pr_global ref =
   [< 'sTR (string_of_qualid (Global.qualid_of_global ref)) >]