diff options
Diffstat (limited to 'parsing/prettyp.mli')
| -rw-r--r-- | parsing/prettyp.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/parsing/prettyp.mli b/parsing/prettyp.mli index 20429cd3d..4c52420d0 100644 --- a/parsing/prettyp.mli +++ b/parsing/prettyp.mli @@ -57,7 +57,7 @@ val print_graph : unit -> std_ppcmds val print_classes : unit -> std_ppcmds val print_coercions : unit -> std_ppcmds val print_path_between : Classops.cl_typ -> Classops.cl_typ -> std_ppcmds -val print_canonical_structures : unit -> std_ppcmds +val print_canonical_projections : unit -> std_ppcmds val inspect : int -> std_ppcmds |