diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-12-17 20:22:37 +0100 |
|---|---|---|
| committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-12-17 20:24:23 +0100 |
| commit | 7ebe6117789ac3c0d31c8a6ed918fce71b6d2e4b (patch) | |
| tree | 2eb3095e1f80082cde506c286c280ca412eebdca /checker/univ.mli | |
| parent | 6b2ec938010c50dae3ec6c87ff8ea7f2a4012b92 (diff) | |
checker: Change in library on disk values, now using context_sets instead of
constraints only.
Diffstat (limited to 'checker/univ.mli')
| -rw-r--r-- | checker/univ.mli | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/checker/univ.mli b/checker/univ.mli index 89dd64486..a4a3a9cb1 100644 --- a/checker/univ.mli +++ b/checker/univ.mli @@ -188,7 +188,15 @@ sig end +module ContextSet : + sig + type t + val empty : t + val constraints : t -> constraints + end + type universe_context = UContext.t +type universe_context_set = ContextSet.t val empty_level_subst : universe_level_subst val is_empty_level_subst : universe_level_subst -> bool |