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

1 files changed, 2 insertions, 5 deletions

diff --git a/parsing/printer.ml b/parsing/printer.ml
index 25578ad761..5169b8d3b3 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)) >]