diff options
| author | Hugo Herbelin | 2020-03-19 13:35:22 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2020-03-19 13:35:22 +0100 |
| commit | 3ae4231d30edfa928595b6fa886ce6df1a495089 (patch) | |
| tree | d6c1d749e6435570e3437f012aad8e6d6797c432 /printing/proof_diffs.ml | |
| parent | 1d8698e97dee385151ef92efd924560b296f8d50 (diff) | |
| parent | ea16c402392722a44bf2227aef7ff73faef70d3a (diff) | |
Merge PR #11795: Print implicit arguments in types of references
Ack-by: herbelin
Diffstat (limited to 'printing/proof_diffs.ml')
| -rw-r--r-- | printing/proof_diffs.ml | 4 |
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 |