diff options
| author | Gaëtan Gilbert | 2019-02-08 15:36:54 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-02-08 15:36:54 +0100 |
| commit | 8c1c7601674f150a969223c67f3e963141b07b4f (patch) | |
| tree | 776a88fc174020962118febce7c3658d51c909ce /dev | |
| parent | bb967f18247fc79c7158a89a1fe160a558910460 (diff) | |
| parent | e3c44130c7700fcffa0cbaf6a0a15a003c209874 (diff) | |
Merge PR #9504: Add print_pure_econstr signature
Reviewed-by: SkySkimmer
Diffstat (limited to 'dev')
| -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 5eac3e2b9c..4d874cdd12 100644 --- a/dev/top_printers.mli +++ b/dev/top_printers.mli @@ -161,6 +161,7 @@ val ppobj : Libobject.obj -> unit val cast_kind_display : Constr.cast_kind -> string val constr_display : Constr.constr -> unit val print_pure_constr : Constr.types -> unit +val print_pure_econstr : EConstr.types -> unit val pploc : Loc.t -> unit |