From cfbfe13f5b515ae2e3c6cdd97e2ccee03bc26e56 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Sun, 1 Feb 2009 00:54:40 +0100 Subject: Imported Upstream version 8.2~rc2+dfsg --- parsing/printer.ml | 19 +++++++++++-------- 1 file changed, 11 insertions(+), 8 deletions(-) (limited to 'parsing/printer.ml') diff --git a/parsing/printer.ml b/parsing/printer.ml index b126cc9c..10034dd9 100644 --- a/parsing/printer.ml +++ b/parsing/printer.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: printer.ml 11309 2008-08-06 10:30:35Z herbelin $ *) +(* $Id: printer.ml 11739 2009-01-02 19:33:19Z herbelin $ *) open Pp open Util @@ -90,14 +90,14 @@ let pr_cases_pattern t = pr_cases_pattern_expr (extern_cases_pattern Idset.empty t) let pr_lconstr_pattern_env env c = - pr_lconstr_expr (extern_constr_pattern (names_of_rel_context env) c) + pr_lconstr_pattern_expr (extern_constr_pattern (names_of_rel_context env) c) let pr_constr_pattern_env env c = - pr_constr_expr (extern_constr_pattern (names_of_rel_context env) c) + pr_constr_pattern_expr (extern_constr_pattern (names_of_rel_context env) c) let pr_lconstr_pattern t = - pr_lconstr_expr (extern_constr_pattern empty_names_context t) + pr_lconstr_pattern_expr (extern_constr_pattern empty_names_context t) let pr_constr_pattern t = - pr_constr_expr (extern_constr_pattern empty_names_context t) + pr_constr_pattern_expr (extern_constr_pattern empty_names_context t) let pr_sort s = pr_rawsort (extern_sort s) @@ -162,9 +162,9 @@ let pr_rel_decl env (na,c,typ) = (* Prints a signature, all declarations on the same line if possible *) let pr_named_context_of env = - hv 0 (fold_named_context - (fun env d pps -> pps ++ ws 2 ++ pr_var_decl env d) - env ~init:(mt ())) + let make_decl_list env d pps = pr_var_decl env d :: pps in + let psl = List.rev (fold_named_context make_decl_list env ~init:[]) in + hv 0 (prlist_with_sep (fun _ -> ws 2) (fun x -> x) psl) let pr_named_context env ne_context = hv 0 (Sign.fold_named_context @@ -475,6 +475,9 @@ let pr_prim_rule = function (str (if withdep then "dependent " else "") ++ str"move " ++ pr_id id1 ++ pr_move_location pr_id id2) + | Order ord -> + (str"order " ++ prlist_with_sep pr_spc pr_id ord) + | Rename (id1,id2) -> (str "rename " ++ pr_id id1 ++ str " into " ++ pr_id id2) -- cgit v1.2.3