blob: bca43697cb30f0f1d8b6e3c88e2f5022d06fad93 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
|
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
(* v * Copyright INRIA, CNRS and contributors *)
(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
(** Monomorphic universes need to survive sections. *)
let name_instance inst =
let map lvl = match Univ.Level.name lvl with
| None -> (* Having Prop/Set/Var as section universes makes no sense *)
assert false
| Some na ->
try
let qid = Nametab.shortest_qualid_of_universe Names.Id.Set.empty na in
Names.Name (Libnames.qualid_basename qid)
with Not_found ->
(* Best-effort naming from the string representation of the level.
See univNames.ml for a similar hack. *)
Names.Name (Names.Id.of_string_soft (Univ.Level.to_string lvl))
in
Array.map map (Univ.Instance.to_array inst)
let declare_universe_context ~poly ctx =
if poly then
let uctx = Univ.ContextSet.to_context ctx in
let nas = name_instance (Univ.UContext.instance uctx) in
Global.push_section_context (nas, uctx)
else
Global.push_context_set ~strict:true ctx
|
