diff options
| author | Gaëtan Gilbert | 2021-02-26 18:01:28 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2021-02-26 18:01:28 +0100 |
| commit | 3abde17c1117d9c413a9d4ad3e0af3d71e77fdb4 (patch) | |
| tree | ba512d7e9d024ce15b794983d92af62f7405573d | |
| parent | 15074f171cdf250880bd0f7a2806356040c89f36 (diff) | |
Expose Top_printers.econstr_display
| -rw-r--r-- | dev/top_printers.mli | 1 |
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 |