aboutsummaryrefslogtreecommitdiff
path: root/dev
diff options
context:
space:
mode:
authorcoqbot-app[bot]2021-02-26 18:07:01 +0000
committerGitHub2021-02-26 18:07:01 +0000
commit4d93cebf19b2ac0ce162dad8c4c73d84ee7f4832 (patch)
treeba512d7e9d024ce15b794983d92af62f7405573d /dev
parent15074f171cdf250880bd0f7a2806356040c89f36 (diff)
parent3abde17c1117d9c413a9d4ad3e0af3d71e77fdb4 (diff)
Merge PR #13883: Expose Top_printers.econstr_display
Reviewed-by: ejgallego
Diffstat (limited to 'dev')
-rw-r--r--dev/top_printers.mli1
1 files changed, 1 insertions, 0 deletions
diff --git a/dev/top_printers.mli b/dev/top_printers.mli
index e8ed6c709e..b4b24d743a 100644
--- a/dev/top_printers.mli
+++ b/dev/top_printers.mli
@@ -165,6 +165,7 @@ val ppobj : Libobject.obj -> unit
(* Some super raw printers *)
val cast_kind_display : Constr.cast_kind -> string
val constr_display : Constr.constr -> unit
+val econstr_display : EConstr.constr -> unit
val print_pure_constr : Constr.types -> unit
val print_pure_econstr : EConstr.types -> unit