diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-12-21 10:36:03 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-12-21 10:36:03 +0000 |
| commit | 691b79b3ef0d78c414b2c7c647524eb1bc1d94dd (patch) | |
| tree | e2fdb6cca2bb79374cb17c3f86ff100cd122fc9d /proofs | |
| parent | edfc0dd4667f6d925f6492f593d51cd157cae620 (diff) | |
code mort
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3472 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'proofs')
| -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 |