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

---
 checker/indtypes.ml | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

(limited to 'checker/indtypes.ml')

diff --git a/checker/indtypes.ml b/checker/indtypes.ml
index 22c8438126..bb0db8cfe9 100644
--- a/checker/indtypes.ml
+++ b/checker/indtypes.ml
@@ -586,6 +586,8 @@ let check_inductive env kn mib =
       Univ.AUContext.repr (Univ.ACumulativityInfo.univ_context cumi)
   in
   let env = Environ.push_context ind_ctx env in
+  (** Locally set the oracle for further typechecking *)
+  let env0 = Environ.set_oracle env mib.mind_typing_flags.conv_oracle in
   (* check mind_record : TODO ? check #constructor = 1 ? *)
   (* check mind_finite : always OK *)
   (* check mind_ntypes *)
@@ -593,13 +595,13 @@ let check_inductive env kn mib =
     user_err Pp.(str "not the right number of packets");
   (* check mind_params_ctxt *)
   let params = mib.mind_params_ctxt in
-  let _ = check_ctxt env params in
+  let _ = check_ctxt env0 params in
   (* check mind_nparams *)
   if rel_context_nhyps params <> mib.mind_nparams then
     user_err Pp.(str "number the right number of parameters");
   (* mind_packets *)
   (*  - check arities *)
-  let env_ar = typecheck_arity env params mib.mind_packets in
+  let env_ar = typecheck_arity env0 params mib.mind_packets in
   (*  - check constructor types *)
   Array.iter (typecheck_one_inductive env_ar params mib) mib.mind_packets;
   (* check the inferred subtyping relation *)
-- 
cgit v1.2.3