diff options
| author | Pierre-Marie Pédrot | 2019-08-08 13:48:57 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-09-25 22:14:34 +0200 |
| commit | 4838fd47542018ba61cd096c93edf45b7ef68529 (patch) | |
| tree | 918ec790b3de6b77ef8442532a69db9f2b1a76b1 /library/lib.mli | |
| parent | 227fcc4dff6fbb68ad6b91387b2f36705329a57e (diff) | |
Refine the API to declare section-local universes.
The section local universes are undoubtedly ordered, but the API was requiring
an unordered ContextSet. We also move the naming one level up.
Unfortunately, some callers are currently defining the same polymorphic
universes in a section several times, notably the "Variable" command. I had
to hack around this behaviour.
Diffstat (limited to 'library/lib.mli')
| -rw-r--r-- | library/lib.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/library/lib.mli b/library/lib.mli index 9ffa69ef93..db6df4395b 100644 --- a/library/lib.mli +++ b/library/lib.mli @@ -182,7 +182,7 @@ val section_instance : GlobRef.t -> Univ.Instance.t * Id.t array val is_in_section : GlobRef.t -> bool val add_section_variable : name:Id.t -> poly:bool -> unit -val add_section_context : Univ.ContextSet.t -> unit +val add_section_context : Name.t array * Univ.UContext.t -> unit val add_section_constant : poly:bool -> Constant.t -> Constr.named_context -> unit val add_section_kn : poly:bool -> MutInd.t -> Constr.named_context -> unit val replacement_context : unit -> Opaqueproof.work_list |