From c1630c9dcdf91dc965b3c375d68e3338fb737531 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Thu, 1 Oct 2015 13:32:47 +0200 Subject: Univs: update checker --- checker/environ.mli | 2 ++ 1 file changed, 2 insertions(+) (limited to 'checker/environ.mli') diff --git a/checker/environ.mli b/checker/environ.mli index f3b2dd839..87f143d1b 100644 --- a/checker/environ.mli +++ b/checker/environ.mli @@ -39,6 +39,8 @@ val push_rec_types : name array * constr array * 'a -> env -> env (* Universes *) val universes : env -> Univ.universes val add_constraints : Univ.constraints -> env -> env +val push_context : ?strict:bool -> Univ.universe_context -> env -> env +val push_context_set : ?strict:bool -> Univ.universe_context_set -> env -> env val check_constraints : Univ.constraints -> env -> bool (* Constants *) -- cgit v1.2.3