From cff3c5a7148afc722852bd01658fe49ffec1d967 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Thu, 6 Dec 2018 15:52:37 +0100
Subject: Revise API for global universes.

Rename Univ.Level.{Qualid -> UGlobal}, remove Univ.Level.Id.

Remove the ability to split the argument of `Univ.Level.Level` into a
dirpath*int pair (except by going through string hacks like
detyping/pretyping(/funind) does).

Id.of_string_soft to turn unnamed universes into qualid is pushed up
to detyping. (TODO some followup PR clean up more)

This makes it pointless to have an opaque type for ints in
Univ.Level: it would only be used as argument to
Univ.Level.UGlobal.make, ie
~~~
open Univ.Level
let x = UGlobal.make dp (Id.make n)
(* vs *)
let x = UGlobal.make dp n
~~~

Remaining places which create levels from ints are various hacks (eg
the dummy in inductive.ml, the Type.n universes in ugraph
sort_universes) and univgen.

UnivGen does have an opaque type for ints used as univ ids since they
get manipulated by the stm.

NB: build breaks due to ocamldep issue if UGlobal is named Global instead.
---
 interp/declare.ml | 8 ++------
 1 file changed, 2 insertions(+), 6 deletions(-)

(limited to 'interp')

diff --git a/interp/declare.ml b/interp/declare.ml
index 0c9d26dd01..a809a856b9 100644
--- a/interp/declare.ml
+++ b/interp/declare.ml
@@ -469,7 +469,7 @@ type universe_source =
   | QualifiedUniv of Id.t (* global universe introduced by some global value *)
   | UnqualifiedUniv (* other global universe *)
 
-type universe_name_decl = universe_source * (Id.t * Univ.Level.Qualid.t) list
+type universe_name_decl = universe_source * (Id.t * Univ.Level.UGlobal.t) list
 
 let check_exists sp =
   if Nametab.exists_universe sp then
@@ -540,11 +540,7 @@ let do_universe poly l =
       user_err ~hdr:"Constraint"
                    (str"Cannot declare polymorphic universes outside sections")
   in
-  let l =
-    List.map (fun {CAst.v=id} ->
-      let lev = UnivGen.new_univ_id () in
-      (id, Univ.Level.Qualid.make (Global.current_dirpath ()) lev)) l
-  in
+  let l = List.map (fun {CAst.v=id} -> (id, UnivGen.new_univ_global ())) l in
   let ctx = List.fold_left (fun ctx (_,qid) -> Univ.LSet.add (Univ.Level.make qid) ctx)
       Univ.LSet.empty l, Univ.Constraint.empty
   in
-- 
cgit v1.2.3