diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-08-09 15:51:21 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-08-09 15:59:01 +0200 |
| commit | 56a6727525e860a155b6ae73da152e558b3ea976 (patch) | |
| tree | d4a2c5e3d64fb5c7bbb409f6c89c61dd23b174b6 /kernel/univ.mli | |
| parent | eec72af81a84f7b56b04027693684eebe139a607 (diff) | |
Cleaning up interface of ContextSet.
Names and arguments were uniformized, and some functions were redesigned to
take their typical use-case into account.
Diffstat (limited to 'kernel/univ.mli')
| -rw-r--r-- | kernel/univ.mli | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/kernel/univ.mli b/kernel/univ.mli index 655f87bb5..3779c055d 100644 --- a/kernel/univ.mli +++ b/kernel/univ.mli @@ -340,8 +340,9 @@ sig val union : t -> t -> t val diff : t -> t -> t - val add_constraints : t -> constraints -> t - val add_universes : Instance.t -> t -> t + val add_universe : universe_level -> t -> t + val add_constraints : constraints -> t -> t + val add_instance : Instance.t -> t -> t (** Arbitrary choice of linear order of the variables *) val to_context : t -> universe_context |