diff options
-rw-r--r-- | proofs/tacmach.ml | 18 | ||||
-rw-r--r-- | proofs/tacmach.mli | 1 |
2 files changed, 0 insertions, 19 deletions
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml index 6b53f6c98..51dd1e59d 100644 --- a/proofs/tacmach.ml +++ b/proofs/tacmach.ml @@ -237,24 +237,6 @@ open Printer open Tacexpr open Rawterm -let pr_com sigma goal com = - prterm (rename_bound_var (Global.env()) - (ids_of_named_context goal.evar_hyps) - (Constrintern.interp_constr sigma (Evarutil.evar_env goal) com)) - -let pr_one_binding sigma goal = function - | (NamedHyp id,com) -> pr_id id ++ str ":=" ++ pr_com sigma goal com - | (AnonHyp n,com) -> int n ++ str ":=" ++ pr_com sigma goal com - -let pr_bindings sigma goal lb = - let prf = pr_one_binding sigma goal in - match lb with - | ImplicitBindings l -> - str "with" ++ spc () ++ prlist_with_sep pr_spc (pr_com sigma goal) l - | ExplicitBindings l -> - str "with" ++ spc () ++ prlist_with_sep pr_spc prf l - | NoBindings -> mt () - let rec pr_list f = function | [] -> mt () | a::l1 -> (f a) ++ pr_list f l1 diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli index 5ea42b380..828b6b146 100644 --- a/proofs/tacmach.mli +++ b/proofs/tacmach.mli @@ -176,6 +176,5 @@ val tclIDTAC_list : tactic_list open Pp (*i*) -val pr_com : evar_map -> goal -> Topconstr.constr_expr -> std_ppcmds val pr_gls : goal sigma -> std_ppcmds val pr_glls : goal list sigma -> std_ppcmds |