From 50ad4221263d1a3243541a1108e447ac3c1b3742 Mon Sep 17 00:00:00 2001
From: SimonBoulier
Date: Mon, 9 Mar 2020 19:33:15 +0100
Subject: Print implicit arguments in types of references

---
 printing/printer.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'printing/printer.ml')

diff --git a/printing/printer.ml b/printing/printer.ml
index b376616b61..88ca0616dd 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)
-- 
cgit v1.2.3