diff options
-rwxr-xr-x | parsing/ast.ml | 7 | ||||
-rw-r--r-- | parsing/printer.ml | 7 |
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)) >] |