aboutsummaryrefslogtreecommitdiff
path: root/printing/proof_diffs.ml
diff options
context:
space:
mode:
Diffstat (limited to 'printing/proof_diffs.ml')
-rw-r--r--printing/proof_diffs.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/printing/proof_diffs.ml b/printing/proof_diffs.ml
index da76bc130d..fb91ea7b5c 100644
--- a/printing/proof_diffs.ml
+++ b/printing/proof_diffs.ml
@@ -244,9 +244,9 @@ let process_goal sigma g : EConstr.t reified_goal =
let hyps = List.map to_tuple hyps in
{ name; ty; hyps; env; sigma };;
-let pr_letype_env ?lax ?goal_concl_style env sigma t =
+let pr_letype_env ?lax ?goal_concl_style env sigma ?impargs t =
Ppconstr.pr_lconstr_expr env sigma
- (Constrextern.extern_type ?lax ?goal_concl_style env sigma t)
+ (Constrextern.extern_type ?lax ?goal_concl_style env sigma ?impargs t)
let pp_of_type env sigma ty =
pr_letype_env ~goal_concl_style:true env sigma ty