diff options
Diffstat (limited to 'parsing/printer.mli')
-rw-r--r-- | parsing/printer.mli | 3 |
1 files changed, 0 insertions, 3 deletions
diff --git a/parsing/printer.mli b/parsing/printer.mli index 01b691a13..8be938f81 100644 --- a/parsing/printer.mli +++ b/parsing/printer.mli @@ -24,9 +24,6 @@ open Proof_type (*i*) (* These are the entry points for printing terms, context, tac, ... *) -(* -val gentacpr : Tacexpr.raw_tactic_expr -> std_ppcmds -*) val prterm_env : env -> constr -> std_ppcmds val prterm_env_at_top : env -> constr -> std_ppcmds |