diff options
author | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-06-01 05:42:14 +0200 |
---|---|---|
committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-06-01 05:42:14 +0200 |
commit | a0ea7ebf4838903c3ed9a9b885716cf14134a0c8 (patch) | |
tree | 8a073c4a47c29d0f9b19aec6d28c0c62dbe8a3d5 /plugins/ltac | |
parent | eed90d1bd867dce59f6bf1b2bf769fff188f128b (diff) |
[printing] Remove duplicated printing function.
It seems there were 4 copies of the same function in the code base.
Diffstat (limited to 'plugins/ltac')
-rw-r--r-- | plugins/ltac/pptactic.ml | 54 | ||||
-rw-r--r-- | plugins/ltac/pptactic.mli | 4 |
2 files changed, 4 insertions, 54 deletions
diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml index 4e254ea76..099789061 100644 --- a/plugins/ltac/pptactic.ml +++ b/plugins/ltac/pptactic.ml @@ -161,28 +161,6 @@ type 'a extra_genarg_printer = | AnonHyp n -> int n | NamedHyp id -> pr_id id - let pr_binding prc = function - | loc, (NamedHyp id, c) -> hov 1 (pr_id id ++ str " := " ++ cut () ++ prc c) - | loc, (AnonHyp n, c) -> hov 1 (int n ++ str " := " ++ cut () ++ prc c) - - let pr_bindings prc prlc = function - | ImplicitBindings l -> - brk (1,1) ++ keyword "with" ++ brk (1,1) ++ - hv 0 (prlist_with_sep spc prc l) - | ExplicitBindings l -> - brk (1,1) ++ keyword "with" ++ brk (1,1) ++ - hv 0 (prlist_with_sep spc (fun b -> str"(" ++ pr_binding prlc b ++ str")") l) - | NoBindings -> mt () - - let pr_bindings_no_with prc prlc = function - | ImplicitBindings l -> - brk (0,1) ++ - prlist_with_sep spc prc l - | ExplicitBindings l -> - brk (0,1) ++ - prlist_with_sep spc (fun b -> str"(" ++ pr_binding prlc b ++ str")") l - | NoBindings -> mt () - let pr_clear_flag clear_flag pp x = match clear_flag with | Some false -> surround (pp x) @@ -190,7 +168,7 @@ type 'a extra_genarg_printer = | None -> pp x let pr_with_bindings prc prlc (c,bl) = - prc c ++ pr_bindings prc prlc bl + prc c ++ Miscprint.pr_bindings prc prlc bl let pr_with_bindings_arg prc prlc (clear_flag,c) = pr_clear_flag clear_flag (pr_with_bindings prc prlc) c @@ -367,30 +345,6 @@ type 'a extra_genarg_printer = | EvalConstRef sp -> Nametab.pr_global_env (Termops.vars_of_env env) (Globnames.ConstRef sp) - let pr_esubst prc l = - let pr_qhyp = function - (_,(AnonHyp n,c)) -> str "(" ++ int n ++ str" := " ++ prc c ++ str ")" - | (_,(NamedHyp id,c)) -> - str "(" ++ pr_id id ++ str" := " ++ prc c ++ str ")" - in - prlist_with_sep spc pr_qhyp l - - let pr_bindings_gen for_ex prc prlc = function - | ImplicitBindings l -> - spc () ++ - hv 2 ((if for_ex then mt() else keyword "with" ++ spc ()) ++ - prlist_with_sep spc prc l) - | ExplicitBindings l -> - spc () ++ - hv 2 ((if for_ex then mt() else keyword "with" ++ spc ()) ++ - pr_esubst prlc l) - | NoBindings -> mt () - - let pr_bindings prc prlc = pr_bindings_gen false prc prlc - - let pr_with_bindings prc prlc (c,bl) = - hov 1 (prc c ++ pr_bindings prc prlc bl) - let pr_as_disjunctive_ipat prc ipatl = keyword "as" ++ spc () ++ pr_or_var (fun (loc,p) -> Miscprint.pr_or_and_intro_pattern prc p) ipatl @@ -1280,9 +1234,9 @@ let () = (pr_red_expr (pr_econstr, pr_leconstr, pr_evaluable_reference, pr_constr_pattern)); Genprint.register_print0 wit_quant_hyp pr_quantified_hypothesis pr_quantified_hypothesis pr_quantified_hypothesis; Genprint.register_print0 wit_bindings - (pr_bindings_no_with pr_constr_expr pr_lconstr_expr) - (pr_bindings_no_with (pr_and_constr_expr pr_glob_constr) (pr_and_constr_expr pr_lglob_constr)) - (fun it -> pr_bindings_no_with pr_econstr pr_leconstr (fst (run_delayed it))); + (Miscprint.pr_bindings_no_with pr_constr_expr pr_lconstr_expr) + (Miscprint.pr_bindings_no_with (pr_and_constr_expr pr_glob_constr) (pr_and_constr_expr pr_lglob_constr)) + (fun it -> Miscprint.pr_bindings_no_with pr_econstr pr_leconstr (fst (run_delayed it))); Genprint.register_print0 wit_constr_with_bindings (pr_with_bindings pr_constr_expr pr_lconstr_expr) (pr_with_bindings (pr_and_constr_expr pr_glob_constr) (pr_and_constr_expr pr_lglob_constr)) diff --git a/plugins/ltac/pptactic.mli b/plugins/ltac/pptactic.mli index 19bdf2d49..4265c416b 100644 --- a/plugins/ltac/pptactic.mli +++ b/plugins/ltac/pptactic.mli @@ -106,10 +106,6 @@ val pr_hintbases : string list option -> std_ppcmds val pr_auto_using : ('constr -> std_ppcmds) -> 'constr list -> std_ppcmds -val pr_bindings : - ('constr -> std_ppcmds) -> - ('constr -> std_ppcmds) -> 'constr bindings -> std_ppcmds - val pr_match_pattern : ('a -> std_ppcmds) -> 'a match_pattern -> std_ppcmds val pr_match_rule : bool -> ('a -> std_ppcmds) -> ('b -> std_ppcmds) -> |