aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing/printer.mli
diff options
context:
space:
mode:
Diffstat (limited to 'parsing/printer.mli')
-rw-r--r--parsing/printer.mli3
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