From 9ebf44d84754adc5b64fcf612c6816c02c80462d Mon Sep 17 00:00:00 2001
From: Benjamin Barenblat <bbaren@debian.org>
Date: Sat, 2 Feb 2019 19:29:23 -0500
Subject: Imported Upstream version 8.9.0

---
 library/global.mli | 19 +++++++++++--------
 1 file changed, 11 insertions(+), 8 deletions(-)

(limited to 'library/global.mli')

diff --git a/library/global.mli b/library/global.mli
index b82039a0..2819c187 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -23,13 +23,14 @@ val env_is_initial : unit -> bool
 
 val universes : unit -> UGraph.t
 val named_context_val : unit -> Environ.named_context_val
-val named_context : unit -> Context.Named.t
+val named_context : unit -> Constr.named_context
 
 (** {6 Enriching the global environment } *)
 
 (** Changing the (im)predicativity of the system *)
 val set_engagement : Declarations.engagement -> unit
 val set_typing_flags : Declarations.typing_flags -> unit
+val typing_flags : unit -> Declarations.typing_flags
 
 (** Variables, Local definitions, constants, inductive types *)
 
@@ -79,7 +80,7 @@ val add_module_parameter :
 
 (** {6 Queries in the global environment } *)
 
-val lookup_named     : variable -> Context.Named.Declaration.t
+val lookup_named     : variable -> Constr.named_declaration
 val lookup_constant  : Constant.t -> Declarations.constant_body
 val lookup_inductive : inductive ->
   Declarations.mutual_inductive_body * Declarations.one_inductive_body
@@ -123,26 +124,26 @@ val env_of_context : Environ.named_context_val -> Environ.env
 val join_safe_environment : ?except:Future.UUIDSet.t -> unit -> unit
 val is_joined_environment : unit -> bool
 
-val is_polymorphic : Globnames.global_reference -> bool
-val is_template_polymorphic : Globnames.global_reference -> bool
-val is_type_in_type : Globnames.global_reference -> bool
+val is_polymorphic : GlobRef.t -> bool
+val is_template_polymorphic : GlobRef.t -> bool
+val is_type_in_type : GlobRef.t -> bool
 
 val constr_of_global_in_context : Environ.env ->
-  Globnames.global_reference -> Constr.types * Univ.AUContext.t
+  GlobRef.t -> Constr.types * Univ.AUContext.t
 (** Returns the type of the constant in its local universe
     context. The type should not be used without pushing it's universe
     context in the environmnent of usage. For non-universe-polymorphic
     constants, it does not matter. *)
 
 val type_of_global_in_context : Environ.env -> 
-  Globnames.global_reference -> Constr.types * Univ.AUContext.t
+  GlobRef.t -> Constr.types * Univ.AUContext.t
 (** Returns the type of the constant in its local universe
     context. The type should not be used without pushing it's universe
     context in the environmnent of usage. For non-universe-polymorphic
     constants, it does not matter. *)
 
 (** Returns the universe context of the global reference (whatever its polymorphic status is). *)
-val universes_of_global : Globnames.global_reference -> Univ.AUContext.t
+val universes_of_global : GlobRef.t -> Univ.AUContext.t
 
 (** {6 Retroknowledge } *)
 
@@ -155,6 +156,8 @@ val register_inline : Constant.t -> unit
 
 val set_strategy : Constant.t Names.tableKey -> Conv_oracle.level -> unit
 
+val set_reduction_sharing : bool -> unit
+
 (* Modifies the global state, registering new universes *)
 
 val current_modpath : unit -> ModPath.t
-- 
cgit v1.2.3