diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2015-10-01 13:32:47 +0200 |
|---|---|---|
| committer |  Matthieu Sozeau <mattam@mattam.org> | 2015-10-02 15:54:13 +0200 |
| commit | c1630c9dcdf91dc965b3c375d68e3338fb737531 (patch) | |
| tree | bf77e70bf7f401ff83563f50621712955b7aa618 /checker/univ.mli | |
| parent | 67bdc25eb69ecd485ae1c8fa2dd71d1933f355d0 (diff) | |
Univs: update checker
Diffstat (limited to 'checker/univ.mli')
| -rw-r--r-- | checker/univ.mli | 15 |
1 files changed, 14 insertions, 1 deletions
diff --git a/checker/univ.mli b/checker/univ.mli index 742ef91ae..459adfcd6 100644 --- a/checker/univ.mli +++ b/checker/univ.mli @@ -74,6 +74,13 @@ val check_eq : universe check_function (** The initial graph of universes: Prop < Set *) val initial_universes : universes +(** Adds a universe to the graph, ensuring it is >= or > Set. + @raises AlreadyDeclared if the level is already declared in the graph. *) + +exception AlreadyDeclared + +val add_universe : universe_level -> bool -> universes -> universes + (** {6 Constraints. } *) type constraint_type = Lt | Le | Eq @@ -117,7 +124,7 @@ type univ_inconsistency = constraint_type * universe * universe exception UniverseInconsistency of univ_inconsistency val merge_constraints : constraints -> universes -> universes - + val check_constraints : constraints -> universes -> bool (** {6 Support for universe polymorphism } *) @@ -193,6 +200,9 @@ module ContextSet : type universe_context = UContext.t type universe_context_set = ContextSet.t +val merge_context : bool -> universe_context -> universes -> universes +val merge_context_set : bool -> universe_context_set -> universes -> universes + val empty_level_subst : universe_level_subst val is_empty_level_subst : universe_level_subst -> bool @@ -219,6 +229,9 @@ val subst_instance_constraints : universe_instance -> constraints -> constraints val instantiate_univ_context : universe_context -> universe_context val instantiate_univ_constraints : universe_instance -> universe_context -> constraints +(** Build the relative instance corresponding to the context *) +val make_abstract_instance : universe_context -> universe_instance + (** {6 Pretty-printing of universes. } *) val pr_universes : universes -> Pp.std_ppcmds |