Fix typing_flags in the checker

Now all relevant typing_flags are taken in account by the checker.
The different forms of assumptions are now printed by the checker.

1 files changed, 6 insertions, 2 deletions

diff --git a/checker/checkInductive.ml b/checker/checkInductive.ml
index f2df99dcd6..d20eea7874 100644
--- a/checker/checkInductive.ml
+++ b/checker/checkInductive.ml
@@ -142,8 +142,12 @@ let check_inductive env mind mb =
         mind_universes; mind_variance;
         mind_private; mind_typing_flags; }
     =
-    (* Locally set the oracle for further typechecking *)
-    let env = Environ.set_oracle env mb.mind_typing_flags.conv_oracle in
+    (* Locally set typing flags for further typechecking *)
+    let mb_flags = mb.mind_typing_flags in
+    let env = Environ.set_typing_flags {env.env_typing_flags with check_guarded = mb_flags.check_guarded;
+                                                                  check_positive = mb_flags.check_positive;
+                                                                  check_universes = mb_flags.check_universes;
+                                                                  conv_oracle = mb_flags.conv_oracle} env in
     Indtypes.check_inductive env mind entry
   in
   let check = check mind in