diff options
Diffstat (limited to 'printing/printer.mli')
| -rw-r--r-- | printing/printer.mli | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/printing/printer.mli b/printing/printer.mli index 8fb802cce5..47dfa32b9c 100644 --- a/printing/printer.mli +++ b/printing/printer.mli @@ -70,6 +70,10 @@ val pr_cases_pattern : cases_pattern -> std_ppcmds val pr_sort : sorts -> std_ppcmds +(** Universe constraints *) + +val pr_univ_cstr : Univ.constraints -> std_ppcmds + (** Printing global references using names as short as possible *) val pr_global_env : Idset.t -> global_reference -> std_ppcmds |