aboutsummaryrefslogtreecommitdiff
path: root/printing/printer.mli
diff options
context:
space:
mode:
Diffstat (limited to 'printing/printer.mli')
-rw-r--r--printing/printer.mli4
1 files changed, 2 insertions, 2 deletions
diff --git a/printing/printer.mli b/printing/printer.mli
index ea388ae57e..732af5570d 100644
--- a/printing/printer.mli
+++ b/printing/printer.mli
@@ -107,9 +107,9 @@ val pr_closed_glob_env : ?lax:bool -> ?goal_concl_style:bool -> ?inctx:bool
val pr_ljudge_env : env -> evar_map -> EConstr.unsafe_judgment -> Pp.t * Pp.t
-val pr_lglob_constr_env : env -> 'a glob_constr_g -> Pp.t
+val pr_lglob_constr_env : env -> evar_map -> 'a glob_constr_g -> Pp.t
-val pr_glob_constr_env : env -> 'a glob_constr_g -> Pp.t
+val pr_glob_constr_env : env -> evar_map -> 'a glob_constr_g -> Pp.t
val pr_lconstr_pattern_env : env -> evar_map -> constr_pattern -> Pp.t