From 20c98eab851210702b39e1c66e005acfc351d8dd Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Fri, 1 Dec 2017 10:11:41 +0100 Subject: Proper nametab handling of global universe names They are now bound at the library + module level and can be qualified and shadowed according to the usual rules of qualified names. Parsing and printing of universes "u+n" done as well. In sections, global universes are discharged as well, checking that they can be defined globally when they are introduced --- engine/termops.mli | 2 ++ 1 file changed, 2 insertions(+) (limited to 'engine/termops.mli') diff --git a/engine/termops.mli b/engine/termops.mli index c9a530076..c1600abe8 100644 --- a/engine/termops.mli +++ b/engine/termops.mli @@ -271,6 +271,8 @@ val is_Prop : Evd.evar_map -> constr -> bool val is_Set : Evd.evar_map -> constr -> bool val is_Type : Evd.evar_map -> constr -> bool +val reference_of_level : Evd.evar_map -> Univ.Level.t -> Libnames.reference + (** Combinators on judgments *) val on_judgment : ('a -> 'b) -> ('a, 'a) punsafe_judgment -> ('b, 'b) punsafe_judgment -- cgit v1.2.3