From 7f9223bf9939a626b0813ecc6c34b4ef19b123f0 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 14 Jan 2018 01:14:27 +0100
Subject: Store the conversion oracle in constant and inductive definitions.

We also have to update the checker to deserialize this additional data,
but it is not using it in type-checking yet.
---
 kernel/declarations.ml | 1 +
 kernel/declareops.ml   | 3 ++-
 kernel/declareops.mli  | 2 +-
 kernel/environ.ml      | 6 ++++--
 kernel/pre_env.ml      | 4 +---
 kernel/pre_env.mli     | 1 -
 6 files changed, 9 insertions(+), 8 deletions(-)

(limited to 'kernel')

diff --git a/kernel/declarations.ml b/kernel/declarations.ml
index 7f4b85fd05..5b9e1a1414 100644
--- a/kernel/declarations.ml
+++ b/kernel/declarations.ml
@@ -74,6 +74,7 @@ type typing_flags = {
   check_guarded : bool; (** If [false] then fixed points and co-fixed
                             points are assumed to be total. *)
   check_universes : bool; (** If [false] universe constraints are not checked *)
+  conv_oracle : Conv_oracle.oracle; (** Unfolding strategies for conversion *)
 }
 
 (* some contraints are in constant_constraints, some other may be in
diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index d8768a0fc5..9eed9efcbd 100644
--- a/kernel/declareops.ml
+++ b/kernel/declareops.ml
@@ -15,9 +15,10 @@ module RelDecl = Context.Rel.Declaration
 (** Operations concernings types in [Declarations] :
     [constant_body], [mutual_inductive_body], [module_body] ... *)
 
-let safe_flags = {
+let safe_flags oracle = {
   check_guarded = true;
   check_universes = true;
+  conv_oracle = oracle;
 }
 
 (** {6 Arities } *)
diff --git a/kernel/declareops.mli b/kernel/declareops.mli
index 198831848e..0eed11f49c 100644
--- a/kernel/declareops.mli
+++ b/kernel/declareops.mli
@@ -67,7 +67,7 @@ val inductive_is_cumulative : mutual_inductive_body -> bool
 (** {6 Kernel flags} *)
 
 (** A default, safe set of flags for kernel type-checking *)
-val safe_flags : typing_flags
+val safe_flags : Conv_oracle.oracle -> typing_flags
 
 (** {6 Hash-consing} *)
 
diff --git a/kernel/environ.ml b/kernel/environ.ml
index 1afab453ac..3c86129fed 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -37,8 +37,10 @@ type env = Pre_env.env
 
 let pre_env env = env
 let env_of_pre_env env = env
-let oracle env = env.env_conv_oracle
-let set_oracle env o = { env with env_conv_oracle = o }
+let oracle env = env.env_typing_flags.conv_oracle
+let set_oracle env o =
+  let env_typing_flags = { env.env_typing_flags with conv_oracle = o } in
+  { env with env_typing_flags }
 
 let empty_named_context_val = empty_named_context_val
 
diff --git a/kernel/pre_env.ml b/kernel/pre_env.ml
index c5254b453a..4ef89f8c0e 100644
--- a/kernel/pre_env.ml
+++ b/kernel/pre_env.ml
@@ -75,7 +75,6 @@ type env = {
   env_nb_rel        : int;
   env_stratification : stratification;
   env_typing_flags  : typing_flags;
-  env_conv_oracle   : Conv_oracle.oracle;
   retroknowledge : Retroknowledge.retroknowledge;
   indirect_pterms : Opaqueproof.opaquetab;
 }
@@ -98,8 +97,7 @@ let empty_env = {
   env_stratification = {
     env_universes = UGraph.initial_universes;
     env_engagement = PredicativeSet };
-  env_typing_flags = Declareops.safe_flags;
-  env_conv_oracle = Conv_oracle.empty;
+  env_typing_flags = Declareops.safe_flags Conv_oracle.empty;
   retroknowledge = Retroknowledge.initial_retroknowledge;
   indirect_pterms = Opaqueproof.empty_opaquetab }
 
diff --git a/kernel/pre_env.mli b/kernel/pre_env.mli
index 054ae17437..fef530c872 100644
--- a/kernel/pre_env.mli
+++ b/kernel/pre_env.mli
@@ -53,7 +53,6 @@ type env = {
     env_nb_rel        : int;
     env_stratification : stratification;
     env_typing_flags  : typing_flags;
-    env_conv_oracle   : Conv_oracle.oracle;
     retroknowledge : Retroknowledge.retroknowledge;
     indirect_pterms : Opaqueproof.opaquetab;
 }
-- 
cgit v1.2.3