aboutsummaryrefslogtreecommitdiff
path: root/dev/top_printers.ml
diff options
context:
space:
mode:
authorSimonBoulier2020-03-09 19:33:15 +0100
committerSimonBoulier2020-03-12 11:22:50 +0100
commit50ad4221263d1a3243541a1108e447ac3c1b3742 (patch)
treef0317bc5a2ffd09e8c44eb6f02a403e6ab4d737d /dev/top_printers.ml
parentdbd3a4c4213b3d56908a8387de93e27aaec501a4 (diff)
Print implicit arguments in types of references
Diffstat (limited to 'dev/top_printers.ml')
-rw-r--r--dev/top_printers.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index e8129938a1..2df602967b 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -82,7 +82,7 @@ let ppsconstr x = ppconstr (Mod_subst.force_constr x)
let ppconstr_univ x = Constrextern.with_universes ppconstr x
let ppglob_constr = (fun x -> pp(pr_lglob_constr_env (Global.env()) x))
let pppattern = (fun x -> pp(envpp pr_constr_pattern_env x))
-let pptype = (fun x -> try pp(envpp pr_ltype_env x) with e -> pp (str (Printexc.to_string e)))
+let pptype = (fun x -> try pp(envpp (fun env evm t -> pr_ltype_env env evm t) x) with e -> pp (str (Printexc.to_string e)))
let ppfconstr c = ppconstr (CClosure.term_of_fconstr c)
let ppbigint n = pp (str (Bigint.to_string n));;