diff options
Diffstat (limited to 'proofs/tacmach.mli')
| -rw-r--r-- | proofs/tacmach.mli | 11 |
1 files changed, 3 insertions, 8 deletions
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli index 4793924d7..4fbc102cc 100644 --- a/proofs/tacmach.mli +++ b/proofs/tacmach.mli @@ -172,11 +172,6 @@ val tactic_list_tactic : tactic_list -> tactic val tclFIRSTLIST : tactic_list list -> tactic_list val tclIDTAC_list : tactic_list -(*s Pretty-printing functions. *) - -(*i*) -open Pp -(*i*) - -val pr_gls : goal sigma -> std_ppcmds -val pr_glls : goal list sigma -> std_ppcmds +(*s Pretty-printing functions (debug only). *) +val pr_gls : goal sigma -> Pp.std_ppcmds +val pr_glls : goal list sigma -> Pp.std_ppcmds |