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 --- plugins/romega/const_omega.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'plugins/romega') diff --git a/plugins/romega/const_omega.ml b/plugins/romega/const_omega.ml index 337510ef1..0d491d92b 100644 --- a/plugins/romega/const_omega.ml +++ b/plugins/romega/const_omega.ml @@ -155,7 +155,7 @@ let mk_list univ typ l = loop l let mk_plist = - let type1lev = Universes.new_univ_level (Global.current_dirpath ()) in + let type1lev = Universes.new_univ_level () in fun l -> mk_list type1lev mkProp l let mk_list = mk_list Univ.Level.set -- cgit v1.2.3