diff options
Diffstat (limited to 'library/universes.mli')
| -rw-r--r-- | library/universes.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/library/universes.mli b/library/universes.mli index 150686d739..ab217e8728 100644 --- a/library/universes.mli +++ b/library/universes.mli @@ -171,7 +171,7 @@ val pr_universe_opt_subst : universe_opt_subst -> Pp.std_ppcmds val universes_of_constr : constr -> universe_set val shrink_universe_context : universe_context_set -> universe_set -> universe_context_set val restrict_universe_context : universe_context_set -> universe_set -> universe_context_set -val simplify_universe_context : universe_context_set -> universe_set -> +val simplify_universe_context : universe_context_set -> universe_context_set * universe_level_subst val refresh_constraints : universes -> universe_context_set -> universe_context_set * universes |