diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/univ.mli | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/kernel/univ.mli b/kernel/univ.mli index 990460f9bb..56442cbccd 100644 --- a/kernel/univ.mli +++ b/kernel/univ.mli @@ -52,8 +52,6 @@ val merge_constraints : constraints -> universes -> universes val pr_uni : universe -> Pp.std_ppcmds val pr_universes : universes -> Pp.std_ppcmds -val string_of_univ : universe -> string - (*s Dumping to a file *) val dump_universes : out_channel -> universes -> unit |