diff options
| author | Hugo Herbelin | 2019-12-23 22:57:20 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2019-12-23 22:57:20 +0100 |
| commit | 028d64fb5c461e32752b0f8a92d4e2eca2a26d0d (patch) | |
| tree | 8380a901d2c066536f38552f67ffa76f0e3364b3 /dev/top_printers.mli | |
| parent | 3b9763487f96d308f6339c7eb4fc834b069f6e40 (diff) | |
| parent | cc3ded87f0f440eac2746d59b7aeba60ca9f691f (diff) | |
Merge PR #11293: Rename files with Class in their name to make their role clearer.
Diffstat (limited to 'dev/top_printers.mli')
| -rw-r--r-- | dev/top_printers.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/dev/top_printers.mli b/dev/top_printers.mli index 5a2144f996..133326523b 100644 --- a/dev/top_printers.mli +++ b/dev/top_printers.mli @@ -29,7 +29,7 @@ val ppind : Names.inductive -> unit val ppsp : Libnames.full_path -> unit val ppqualid : Libnames.qualid -> unit -val ppclindex : Classops.cl_index -> unit +val ppclindex : Coercionops.cl_index -> unit val ppscheme : 'a Ind_tables.scheme_kind -> unit |