diff options
Diffstat (limited to 'engine')
| -rw-r--r-- | engine/termops.mli | 2 | ||||
| -rw-r--r-- | engine/uState.ml | 6 | ||||
| -rw-r--r-- | engine/uState.mli | 2 | ||||
| -rw-r--r-- | engine/univGen.ml | 9 | ||||
| -rw-r--r-- | engine/univGen.mli | 6 | ||||
| -rw-r--r-- | engine/univNames.ml | 17 | ||||
| -rw-r--r-- | engine/univNames.mli | 2 |
7 files changed, 24 insertions, 20 deletions
diff --git a/engine/termops.mli b/engine/termops.mli index eef8452e64..7920af8e0e 100644 --- a/engine/termops.mli +++ b/engine/termops.mli @@ -290,7 +290,7 @@ 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.qualid +val reference_of_level : Evd.evar_map -> Univ.Level.t -> Libnames.qualid option (** Combinators on judgments *) diff --git a/engine/uState.ml b/engine/uState.ml index 56b7a16ace..185283225c 100644 --- a/engine/uState.ml +++ b/engine/uState.ml @@ -324,12 +324,14 @@ let constrain_variables diff ctx = let qualid_of_level uctx = let map, map_rev = uctx.uctx_names in fun l -> - try Libnames.qualid_of_ident (Option.get (Univ.LMap.find l map_rev).uname) + try Some (Libnames.qualid_of_ident (Option.get (Univ.LMap.find l map_rev).uname)) with Not_found | Option.IsNone -> UnivNames.qualid_of_level l let pr_uctx_level uctx l = - Libnames.pr_qualid (qualid_of_level uctx l) + match qualid_of_level uctx l with + | Some qid -> Libnames.pr_qualid qid + | None -> Univ.Level.pr l type ('a, 'b) gen_universe_decl = { univdecl_instance : 'a; (* Declared universes *) diff --git a/engine/uState.mli b/engine/uState.mli index ad0cd5c1bb..5170184ef4 100644 --- a/engine/uState.mli +++ b/engine/uState.mli @@ -188,6 +188,6 @@ val update_sigma_env : t -> Environ.env -> t (** {5 Pretty-printing} *) val pr_uctx_level : t -> Univ.Level.t -> Pp.t -val qualid_of_level : t -> Univ.Level.t -> Libnames.qualid +val qualid_of_level : t -> Univ.Level.t -> Libnames.qualid option val pr_weak : (Univ.Level.t -> Pp.t) -> t -> Pp.t diff --git a/engine/univGen.ml b/engine/univGen.ml index 5aa4734b23..40c4c909fe 100644 --- a/engine/univGen.ml +++ b/engine/univGen.ml @@ -13,14 +13,17 @@ open Names open Constr open Univ +type univ_unique_id = int (* Generator of levels *) let new_univ_id, set_remote_new_univ_id = RemoteCounter.new_counter ~name:"Universes" 0 ~incr:((+) 1) - ~build:(fun n -> Level.Id.make n) + ~build:(fun n -> n) + +let new_univ_global () = + Univ.Level.UGlobal.make (Global.current_dirpath ()) (new_univ_id ()) let fresh_level () = - let id = new_univ_id () in - Univ.Level.make2 (Global.current_dirpath ()) id + Univ.Level.make (new_univ_global ()) (* TODO: remove *) let new_univ () = Univ.Universe.make (fresh_level ()) diff --git a/engine/univGen.mli b/engine/univGen.mli index 66e80368a4..b4598e10d0 100644 --- a/engine/univGen.mli +++ b/engine/univGen.mli @@ -15,11 +15,13 @@ open Univ (** The global universe counter *) -val set_remote_new_univ_id : Level.Id.t RemoteCounter.installer +type univ_unique_id +val set_remote_new_univ_id : univ_unique_id RemoteCounter.installer +val new_univ_id : unit -> univ_unique_id (** for the stm *) (** Side-effecting functions creating new universe levels. *) -val new_univ_id : unit -> Level.Id.t +val new_univ_global : unit -> Level.UGlobal.t val fresh_level : unit -> Level.t val new_univ : unit -> Universe.t diff --git a/engine/univNames.ml b/engine/univNames.ml index 6bf1187b65..19705f9d36 100644 --- a/engine/univNames.ml +++ b/engine/univNames.ml @@ -16,17 +16,14 @@ open Univ let qualid_of_level l = match Level.name l with | Some qid -> - begin - try Nametab.shortest_qualid_of_universe qid - with Not_found -> - let (dp,n) = Level.Qualid.repr qid in - let name = Id.of_string_soft (Level.Id.to_string n) in - Libnames.make_qualid dp name - end - | None -> - Libnames.qualid_of_ident @@ Id.of_string_soft (Level.to_string l) + (try Some (Nametab.shortest_qualid_of_universe qid) + with Not_found -> None) + | None -> None -let pr_with_global_universes l = Libnames.pr_qualid (qualid_of_level l) +let pr_with_global_universes l = + match qualid_of_level l with + | Some qid -> Libnames.pr_qualid qid + | None -> Level.pr l (** Global universe information outside the kernel, to handle polymorphic universe names in sections that have to be discharged. *) diff --git a/engine/univNames.mli b/engine/univNames.mli index 6e68153ac2..e9c517babf 100644 --- a/engine/univNames.mli +++ b/engine/univNames.mli @@ -11,7 +11,7 @@ open Univ val pr_with_global_universes : Level.t -> Pp.t -val qualid_of_level : Level.t -> Libnames.qualid +val qualid_of_level : Level.t -> Libnames.qualid option (** Local universe name <-> level mapping *) |