diff options
Diffstat (limited to 'checker/univ.mli')
| -rw-r--r-- | checker/univ.mli | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/checker/univ.mli b/checker/univ.mli index 0eadc6801..21c94d952 100644 --- a/checker/univ.mli +++ b/checker/univ.mli @@ -150,8 +150,6 @@ type universe_level_subst_fn = universe_level -> universe_level type universe_subst = universe universe_map type universe_level_subst = universe_level universe_map -val level_subst_of : universe_subst_fn -> universe_level_subst_fn - (** {6 Universe instances} *) module Instance : |