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/funind/g_indfun.ml4 | |
| 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/funind/g_indfun.ml4')
| -rw-r--r-- | plugins/funind/g_indfun.ml4 | 26 |
1 files changed, 2 insertions, 24 deletions
diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4 index 1db8be081..bd2ac8c67 100644 --- a/plugins/funind/g_indfun.ml4 +++ b/plugins/funind/g_indfun.ml4 @@ -22,26 +22,10 @@ open Pltac DECLARE PLUGIN "recdef_plugin" -let pr_binding prc = function - | loc, (NamedHyp id, c) -> hov 1 (Ppconstr.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) ++ str "with" ++ brk (1,1) ++ - pr_sequence prc l - | ExplicitBindings l -> - brk (1,1) ++ str "with" ++ brk (1,1) ++ - pr_sequence (fun b -> str"(" ++ pr_binding prlc b ++ str")") l - | NoBindings -> mt () - -let pr_with_bindings prc prlc (c,bl) = - prc c ++ hv 0 (pr_bindings prc prlc bl) - let pr_fun_ind_using prc prlc _ opt_c = match opt_c with | None -> mt () - | Some b -> spc () ++ hov 2 (str "using" ++ spc () ++ pr_with_bindings prc prlc b) + | Some b -> spc () ++ hov 2 (str "using" ++ spc () ++ Miscprint.pr_with_bindings prc prlc b) (* Duplication of printing functions because "'a with_bindings" is (internally) not uniform in 'a: indeed constr_with_bindings at the @@ -49,17 +33,12 @@ let pr_fun_ind_using prc prlc _ opt_c = "constr with_bindings"; hence, its printer cannot be polymorphic in (prc,prlc)... *) -let pr_with_bindings_typed prc prlc (c,bl) = - prc c ++ - hv 0 (pr_bindings prc prlc bl) - let pr_fun_ind_using_typed prc prlc _ opt_c = match opt_c with | None -> mt () | Some b -> let (b, _) = Tactics.run_delayed (Global.env ()) Evd.empty b in - spc () ++ hov 2 (str "using" ++ spc () ++ pr_with_bindings_typed prc prlc b) - + spc () ++ hov 2 (str "using" ++ spc () ++ Miscprint.pr_with_bindings prc prlc b) ARGUMENT EXTEND fun_ind_using TYPED AS constr_with_bindings option @@ -80,7 +59,6 @@ TACTIC EXTEND newfuninv ] END - let pr_intro_as_pat _prc _ _ pat = match pat with | Some pat -> |