From 20481a3f3405f04b47c7865ca2788a6f63660443 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>
Date: Sun, 14 Jan 2018 02:20:42 +0100
Subject: Actually use the strategy information in the checker.

---
 checker/environ.ml | 15 +++++++++++++--
 1 file changed, 13 insertions(+), 2 deletions(-)

(limited to 'checker/environ.ml')

diff --git a/checker/environ.ml b/checker/environ.ml
index 9db0d60e8..3830cd0dc 100644
--- a/checker/environ.ml
+++ b/checker/environ.ml
@@ -21,7 +21,15 @@ type env = {
     env_globals       : globals;
     env_rel_context   : rel_context;
     env_stratification : stratification;
-    env_imports : Cic.vodigest MPmap.t }
+    env_imports : Cic.vodigest MPmap.t;
+    env_conv_oracle : oracle; }
+
+let empty_oracle = {
+  var_opacity = Id.Map.empty;
+  cst_opacity = Cmap.empty;
+  var_trstate = Id.Pred.empty;
+  cst_trstate = Cpred.empty;
+}
 
 let empty_env = {
   env_globals =
@@ -34,7 +42,8 @@ let empty_env = {
   env_stratification =
   { env_universes = Univ.initial_universes;
     env_engagement = PredicativeSet };
-  env_imports = MPmap.empty }
+  env_imports = MPmap.empty;
+  env_conv_oracle = empty_oracle }
 
 let engagement env = env.env_stratification.env_engagement
 let universes env = env.env_stratification.env_universes
@@ -51,6 +60,8 @@ let set_engagement (impr_set as c) env =
   { env with env_stratification =
       { env.env_stratification with env_engagement = c } }
 
+let set_oracle env oracle = { env with env_conv_oracle = oracle }
+
 (* Digests *)
 
 let add_digest env dp digest =
-- 
cgit v1.2.3