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
---
 interp/declare.mli | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

(limited to 'interp/declare.mli')

diff --git a/interp/declare.mli b/interp/declare.mli
index d50d37368c..31883c9d78 100644
--- a/interp/declare.mli
+++ b/interp/declare.mli
@@ -87,6 +87,5 @@ val exists_name : Id.t -> bool
 val declare_universe_context : polymorphic -> Univ.ContextSet.t -> unit
 
 val do_universe : polymorphic -> Id.t Loc.located list -> unit
-val do_constraint : polymorphic ->
-  (Misctypes.glob_level * Univ.constraint_type * Misctypes.glob_level) list ->
-  unit
+val do_constraint : polymorphic -> (Misctypes.glob_level * Univ.constraint_type * Misctypes.glob_level) list ->
+                    unit
-- 
cgit v1.2.3


From 4fcf1fa32ff395d6bd5f6ce4803eee18173c4d36 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Wed, 22 Nov 2017 18:39:34 +0100
Subject: Cleanup API for registering universe binders.

- Regularly declared for for polymorphic constants
- Declared globally for monomorphic constants.

  E.g mono@{i} := Type@{i} is printed as
  mono@{mono.i} := Type@{mono.i}.

  There can be a name clash if there's a module and a constant of the
  same name. It is detected and is an error if the constant is first
  but is not detected and the name for the constant not
  registered (??) if the constant comes second.

Accept VarRef when registering universe binders

Fix two problems found by Gaëtan where binders were not registered properly

Simplify API substantially by not passing around a substructure of an
already carrier-around structure in interpretation/declaration code of
constants and proofs

Fix an issue of the stronger restrict universe context + no evd leak

This is uncovered by not having an evd leak in interp_definition, and
the stronger restrict_universe_context. This patch could be backported
to 8.7, it could also be triggered by the previous restrict_context I
think.
---
 interp/declare.mli | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

(limited to 'interp/declare.mli')

diff --git a/interp/declare.mli b/interp/declare.mli
index 31883c9d78..f368d164e9 100644
--- a/interp/declare.mli
+++ b/interp/declare.mli
@@ -80,9 +80,8 @@ val recursive_message : bool (** true = fixpoint *) ->
 
 val exists_name : Id.t -> bool
 
-
-
 (** Global universe contexts, names and constraints *)
+val declare_univ_binders : Globnames.global_reference -> Universes.universe_binders -> unit
 
 val declare_universe_context : polymorphic -> Univ.ContextSet.t -> unit
 
-- 
cgit v1.2.3