diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-09-26 23:57:40 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-09-26 23:57:40 +0200 |
| commit | b9740771e8113cb9e607793887be7a12587d0326 (patch) | |
| tree | f69105ad9813738abd10ae824756947940a7dc6d /kernel | |
| parent | 4b6383889d4d38de4c9a28bee960b30114a51b16 (diff) | |
| parent | 3c964a60d698134c21adc77cbb69ce1528350682 (diff) | |
Merge PR #688: Binding universe constraints in Definition/Inductive/etc...
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/univ.mli | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/kernel/univ.mli b/kernel/univ.mli index a4f2e26b6..94116e473 100644 --- a/kernel/univ.mli +++ b/kernel/univ.mli @@ -411,6 +411,7 @@ sig val add_instance : Instance.t -> t -> t (** Arbitrary choice of linear order of the variables *) + val sort_levels : Level.t array -> Level.t array val to_context : t -> universe_context val of_context : universe_context -> t |