aboutsummaryrefslogtreecommitdiff
path: root/printing/printer.ml
diff options
context:
space:
mode:
Diffstat (limited to 'printing/printer.ml')
-rw-r--r--printing/printer.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/printing/printer.ml b/printing/printer.ml
index 70fdd43908..32dc4bb0f0 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -106,8 +106,8 @@ let pr_letype_env = Proof_diffs.pr_letype_env
let pr_type_env ?lax ?goal_concl_style env sigma c =
pr_etype_env ?lax ?goal_concl_style env sigma (EConstr.of_constr c)
-let pr_ltype_env ?lax ?goal_concl_style env sigma c =
- pr_letype_env ?lax ?goal_concl_style env sigma (EConstr.of_constr c)
+let pr_ltype_env ?lax ?goal_concl_style env sigma ?impargs c =
+ pr_letype_env ?lax ?goal_concl_style env sigma ?impargs (EConstr.of_constr c)
let pr_ljudge_env env sigma j =
(pr_leconstr_env env sigma j.uj_val, pr_leconstr_env env sigma j.uj_type)