Merge PR #8842: Towards seeing Global purely as a wrapper on top of kernel functions

4 files changed, 41 insertions, 2 deletions

diff --git a/kernel/environ.ml b/kernel/environ.ml
index 3b7e3ae544..e341412294 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -440,6 +440,16 @@ let constant_value_and_type env (kn, u) =
 	| Undef _ -> None
       in b', cb.const_type, Univ.Constraint.empty
 
+let body_of_constant_body env cb =
+  let otab = opaque_tables env in
+  match cb.const_body with
+  | Undef _ ->
+     None
+  | Def c ->
+     Some (Mod_subst.force_constr c, Declareops.constant_polymorphic_context cb)
+  | OpaqueDef o ->
+     Some (Opaqueproof.force_proof otab o, Declareops.constant_polymorphic_context cb)
+
 (* These functions should be called under the invariant that [env] 
    already contains the constraints corresponding to the constant 
    application. *)
@@ -694,6 +704,22 @@ let is_polymorphic env r =
   | IndRef ind -> polymorphic_ind ind env
   | ConstructRef cstr -> polymorphic_ind (inductive_of_constructor cstr) env
 
+let is_template_polymorphic env r =
+  let open Names.GlobRef in
+  match r with
+  | VarRef _id -> false
+  | ConstRef _c -> false
+  | IndRef ind -> template_polymorphic_ind ind env
+  | ConstructRef cstr -> template_polymorphic_ind (inductive_of_constructor cstr) env
+
+let is_type_in_type env r =
+  let open Names.GlobRef in
+  match r with
+  | VarRef _id -> false
+  | ConstRef c -> type_in_type_constant c env
+  | IndRef ind -> type_in_type_ind ind env
+  | ConstructRef cstr -> type_in_type_ind (inductive_of_constructor cstr) env
+
 (*spiwack: the following functions assemble the pieces of the retroknowledge
    note that the "consistent" register function is available in the module
    Safetyping, Environ only synchronizes the proactive and the reactive parts*)
diff --git a/kernel/environ.mli b/kernel/environ.mli
index 43bfe7c2fb..0255581749 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -211,6 +211,12 @@ val constant_value_and_type : env -> Constant.t puniverses ->
     polymorphic *)
 val constant_context : env -> Constant.t -> Univ.AUContext.t
 
+(** Returns the body of the constant if it has any, and the polymorphic context
+    it lives in. For monomorphic constant, the latter is empty, and for
+    polymorphic constants, the term contains De Bruijn universe variables that
+    need to be instantiated. *)
+val body_of_constant_body : env -> constant_body -> (Constr.constr * Univ.AUContext.t) option
+
 (* These functions should be called under the invariant that [env] 
    already contains the constraints corresponding to the constant 
    application. *)
@@ -320,6 +326,8 @@ val apply_to_hyp : named_context_val -> variable ->
 val remove_hyps : Id.Set.t -> (Constr.named_declaration -> Constr.named_declaration) -> (lazy_val -> lazy_val) -> named_context_val -> named_context_val
 
 val is_polymorphic : env -> Names.GlobRef.t -> bool
+val is_template_polymorphic : env -> GlobRef.t -> bool
+val is_type_in_type : env -> GlobRef.t -> bool
 
 open Retroknowledge
 (** functions manipulating the retroknowledge 
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 12f9592ab7..779e05ee0c 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -194,6 +194,10 @@ let set_engagement c senv =
 let set_typing_flags c senv =
   { senv with env = Environ.set_typing_flags c senv.env }
 
+let set_share_reduction b senv =
+  let flags = Environ.typing_flags senv.env in
+  set_typing_flags { flags with share_reduction = b } senv
+
 (** Check that the engagement [c] expected by a library matches
     the current (initial) one *)
 let check_engagement env expected_impredicative_set =
@@ -1190,7 +1194,7 @@ loaded by side-effect once and for all (like it is done in OCaml).
 Would this be correct with respect to undo's and stuff ?
 *)
 
-let set_strategy e k l = { e with env =
+let set_strategy k l e = { e with env =
    (Environ.set_oracle e.env
       (Conv_oracle.set_strategy (Environ.oracle e.env) k l)) }
 
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index 26fa91adbd..443b5cfd73 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -137,6 +137,7 @@ val add_constraints :
 (** Setting the type theory flavor *)
 val set_engagement : Declarations.engagement -> safe_transformer0
 val set_typing_flags : Declarations.typing_flags -> safe_transformer0
+val set_share_reduction : bool -> safe_transformer0
 
 (** {6 Interactive module functions } *)
 
@@ -217,4 +218,4 @@ val register :
 val register_inline : Constant.t -> safe_transformer0
 
 val set_strategy :
-  safe_environment -> Names.Constant.t Names.tableKey -> Conv_oracle.level -> safe_environment
+  Names.Constant.t Names.tableKey -> Conv_oracle.level -> safe_transformer0