summaryrefslogtreecommitdiff
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, 1 insertions, 2 deletions
diff --git a/parsing/printer.mli b/parsing/printer.mli
index 2d437c20..bbc3a6ca 100644
--- a/parsing/printer.mli
+++ b/parsing/printer.mli
@@ -26,7 +26,6 @@ open Tacexpr
(** Terms *)
val pr_lconstr_env : env -> constr -> std_ppcmds
-val pr_lconstr_env_at_top : env -> constr -> std_ppcmds
val pr_lconstr : constr -> std_ppcmds
val pr_constr_env : env -> constr -> std_ppcmds
@@ -44,7 +43,7 @@ val pr_constr_under_binders : constr_under_binders -> std_ppcmds
val pr_lconstr_under_binders_env : env -> constr_under_binders -> std_ppcmds
val pr_lconstr_under_binders : constr_under_binders -> std_ppcmds
-val pr_ltype_env_at_top : env -> types -> std_ppcmds
+val pr_goal_concl_style_env : env -> types -> std_ppcmds
val pr_ltype_env : env -> types -> std_ppcmds
val pr_ltype : types -> std_ppcmds