Moving the typing_flags to the environment.

5 files changed, 41 insertions, 40 deletions

diff --git a/toplevel/command.ml b/toplevel/command.ml
index ff43cd495..643b06660 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -145,9 +145,9 @@ let get_locality id = function
 | Local -> true
 | Global -> false
 
-let declare_global_definition ~flags ident ce local k pl imps =
+let declare_global_definition ident ce local k pl imps =
   let local = get_locality ident local in
-  let kn = declare_constant ~flags ident ~local (DefinitionEntry ce, IsDefinition k) in
+  let kn = declare_constant ident ~local (DefinitionEntry ce, IsDefinition k) in
   let gr = ConstRef kn in
   let () = maybe_declare_manual_implicits false gr imps in
   let () = Universes.register_universe_binders gr pl in
@@ -158,7 +158,7 @@ let declare_definition_hook = ref ignore
 let set_declare_definition_hook = (:=) declare_definition_hook
 let get_declare_definition_hook () = !declare_definition_hook
 
-let declare_definition ~flags ident (local, p, k) ce pl imps hook =
+let declare_definition ident (local, p, k) ce pl imps hook =
   let fix_exn = Future.fix_exn_of ce.const_entry_body in
   let () = !declare_definition_hook ce in
   let r = match local with
@@ -175,11 +175,11 @@ let declare_definition ~flags ident (local, p, k) ce pl imps hook =
     in
     gr
   | Discharge | Local | Global ->
-    declare_global_definition ~flags ident ce local k pl imps in
+    declare_global_definition ident ce local k pl imps in
   Lemmas.call_hook fix_exn hook local r
 
 let _ = Obligations.declare_definition_ref :=
-       (fun i k c imps hook -> declare_definition ~flags:Declareops.safe_flags i k c [] imps hook)
+       (fun i k c imps hook -> declare_definition i k c [] imps hook)
 
 let do_definition ident k pl bl red_option c ctypopt hook =
   let (ce, evd, pl', imps as def) =
@@ -203,7 +203,7 @@ let do_definition ident k pl bl red_option c ctypopt hook =
 	ignore(Obligations.add_definition
           ident ~term:c cty ctx ?pl ~implicits:imps ~kind:k ~hook obls)
     else let ce = check_definition def in
-      ignore(declare_definition ~flags:Declareops.safe_flags ident k ce pl' imps
+      ignore(declare_definition ident k ce pl' imps
         (Lemmas.mk_hook
           (fun l r -> Lemmas.call_hook (fun exn -> exn) hook l r;r)))
 
@@ -833,12 +833,12 @@ let interp_fix_body env_rec evdref impls (_,ctx) fix ccl =
 
 let build_fix_type (_,ctx) ccl = it_mkProd_or_LetIn ccl ctx
 
-let declare_fix ~flags ?(opaque = false) (_,poly,_ as kind) pl ctx f ((def,_),eff) t imps =
+let declare_fix ?(opaque = false) (_,poly,_ as kind) pl ctx f ((def,_),eff) t imps =
   let ce = definition_entry ~opaque ~types:t ~poly ~univs:ctx ~eff def in
-  declare_definition ~flags f kind ce pl imps (Lemmas.mk_hook (fun _ r -> r))
+  declare_definition f kind ce pl imps (Lemmas.mk_hook (fun _ r -> r))
 
 let _ = Obligations.declare_fix_ref :=
-  (fun ?opaque k ctx f d t imps -> declare_fix ~flags:Declareops.safe_flags ?opaque k [] ctx f d t imps)
+  (fun ?opaque k ctx f d t imps -> declare_fix ?opaque k [] ctx f d t imps)
 
 let prepare_recursive_declaration fixnames fixtypes fixdefs =
   let defs = List.map (subst_vars (List.rev fixnames)) fixdefs in
@@ -1139,7 +1139,7 @@ let interp_cofixpoint l ntns =
   check_recursive false  env evd fix;
   (fix,pl,Evd.evar_universe_context evd,info)
     
-let declare_fixpoint ~flags local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) indexes ntns =
+let declare_fixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) indexes ntns =
   if List.exists Option.is_empty fixdefs then
     (* Some bodies to define by proof *)
     let thms =
@@ -1159,7 +1159,7 @@ let declare_fixpoint ~flags local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fixim
     let fixdefs = List.map Option.get fixdefs in
     let fixdecls = prepare_recursive_declaration fixnames fixtypes fixdefs in
     let env = Global.env() in
-    let indexes = search_guard ~tflags:flags Loc.ghost env indexes fixdecls in
+    let indexes = search_guard Loc.ghost env indexes fixdecls in
     let fiximps = List.map (fun (n,r,p) -> r) fiximps in
     let vars = Universes.universes_of_constr (mkFix ((indexes,0),fixdecls)) in
     let fixdecls =
@@ -1168,7 +1168,7 @@ let declare_fixpoint ~flags local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fixim
     let evd = Evd.restrict_universe_context evd vars in
     let fixdecls = List.map Safe_typing.mk_pure_proof fixdecls in
     let pl, ctx = Evd.universe_context ?names:pl evd in
-    ignore (List.map4 (declare_fix ~flags (local, poly, Fixpoint) pl ctx)
+    ignore (List.map4 (declare_fix (local, poly, Fixpoint) pl ctx)
 	      fixnames fixdecls fixtypes fiximps);
     (* Declare the recursive definitions *)
     fixpoint_message (Some indexes) fixnames;
@@ -1176,7 +1176,7 @@ let declare_fixpoint ~flags local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fixim
   (* Declare notations *)
   List.iter Metasyntax.add_notation_interpretation ntns
 
-let declare_cofixpoint ~flags local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) ntns =
+let declare_cofixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) ntns =
   if List.exists Option.is_empty fixdefs then
     (* Some bodies to define by proof *)
     let thms =
@@ -1202,7 +1202,7 @@ let declare_cofixpoint ~flags local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fix
     let evd = Evd.from_ctx ctx in
     let evd = Evd.restrict_universe_context evd vars in
     let pl, ctx = Evd.universe_context ?names:pl evd in
-    ignore (List.map4 (declare_fix ~flags (local, poly, CoFixpoint) pl ctx) 
+    ignore (List.map4 (declare_fix (local, poly, CoFixpoint) pl ctx) 
 	      fixnames fixdecls fixtypes fiximps);
     (* Declare the recursive definitions *)
     cofixpoint_message fixnames
@@ -1269,11 +1269,9 @@ let do_program_recursive local p fixkind fixl ntns =
       in
       let indexes = 
         Pretyping.search_guard
-          ~tflags:Declareops.safe_flags
           Loc.ghost (Global.env ()) possible_indexes fixdecls in
       List.iteri (fun i _ ->
           Inductive.check_fix env
-                              ~flags:Declareops.safe_flags
                               ((indexes,i),fixdecls))
         fixl
   end in
@@ -1309,21 +1307,26 @@ let do_program_fixpoint local poly l =
 	errorlabstrm "do_program_fixpoint"
 	  (str "Well-founded fixpoints not allowed in mutually recursive blocks")
 
-let do_fixpoint ~flags local poly l =
+let check_safe () =
+  let open Declarations in
+  let flags = Environ.typing_flags (Global.env ()) in
+  flags.check_universes && flags.check_guarded
+
+let do_fixpoint local poly l =
   if Flags.is_program_mode () then do_program_fixpoint local poly l
   else
     let fixl, ntns = extract_fixpoint_components true l in
     let (_, _, _, info as fix) = interp_fixpoint fixl ntns in
     let possible_indexes =
       List.map compute_possible_guardness_evidences info in
-    declare_fixpoint ~flags local poly fix possible_indexes ntns;
-    if not flags.Declarations.check_guarded then Feedback.feedback Feedback.AddedAxiom else ()
+    declare_fixpoint local poly fix possible_indexes ntns;
+    if not (check_safe ()) then Feedback.feedback Feedback.AddedAxiom else ()
 
-let do_cofixpoint ~flags local poly l =
+let do_cofixpoint local poly l =
   let fixl,ntns = extract_cofixpoint_components l in
     if Flags.is_program_mode () then
       do_program_recursive local poly Obligations.IsCoFixpoint fixl ntns
     else
       let cofix = interp_cofixpoint fixl ntns in
-      declare_cofixpoint ~flags local poly cofix ntns;
-      if not flags.Declarations.check_guarded then Feedback.feedback Feedback.AddedAxiom else ()
+      declare_cofixpoint local poly cofix ntns;
+      if not (check_safe ()) then Feedback.feedback Feedback.AddedAxiom else ()
diff --git a/toplevel/command.mli b/toplevel/command.mli
index 2d27552a1..a5132cc66 100644
--- a/toplevel/command.mli
+++ b/toplevel/command.mli
@@ -36,7 +36,7 @@ val interp_definition :
   constr_expr option -> Safe_typing.private_constants definition_entry * Evd.evar_map * 
       Universes.universe_binders * Impargs.manual_implicits
 
-val declare_definition : flags:Declarations.typing_flags -> Id.t -> definition_kind ->
+val declare_definition : Id.t -> definition_kind ->
   Safe_typing.private_constants definition_entry -> Universes.universe_binders -> Impargs.manual_implicits ->
     Globnames.global_reference Lemmas.declaration_hook -> Globnames.global_reference
 
@@ -150,13 +150,12 @@ val interp_cofixpoint :
 (** Registering fixpoints and cofixpoints in the environment *)
 
 val declare_fixpoint :
-  flags:Declarations.typing_flags ->
   locality -> polymorphic ->
   recursive_preentry * lident list option * Evd.evar_universe_context * 
   (Name.t list * Impargs.manual_implicits * int option) list ->
   lemma_possible_guards -> decl_notation list -> unit
 
-val declare_cofixpoint : flags:Declarations.typing_flags -> locality -> polymorphic -> 
+val declare_cofixpoint : locality -> polymorphic -> 
   recursive_preentry * lident list option * Evd.evar_universe_context * 
   (Name.t list * Impargs.manual_implicits * int option) list ->
   decl_notation list -> unit
@@ -164,16 +163,16 @@ val declare_cofixpoint : flags:Declarations.typing_flags -> locality -> polymorp
 (** Entry points for the vernacular commands Fixpoint and CoFixpoint *)
 
 val do_fixpoint :
-  flags:Declarations.typing_flags -> (* When [false], assume guarded. *)
+  (* When [false], assume guarded. *)
   locality -> polymorphic -> (fixpoint_expr * decl_notation list) list -> unit
 
 val do_cofixpoint :
-  flags:Declarations.typing_flags -> (* When [false], assume guarded. *)
+  (* When [false], assume guarded. *)
   locality -> polymorphic -> (cofixpoint_expr * decl_notation list) list -> unit
 
 (** Utils *)
 
 val check_mutuality : Environ.env -> bool -> (Id.t * types) list -> unit
 
-val declare_fix : flags:Declarations.typing_flags -> ?opaque:bool -> definition_kind -> Universes.universe_binders -> Univ.universe_context -> Id.t ->
+val declare_fix : ?opaque:bool -> definition_kind -> Universes.universe_binders -> Univ.universe_context -> Id.t ->
   Safe_typing.private_constants Entries.proof_output -> types -> Impargs.manual_implicits -> global_reference
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 46fb55b5f..e34f38eb3 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -115,10 +115,11 @@ let _ = at_exit print_memory_stat
 
 let impredicative_set = ref Declarations.PredicativeSet
 let set_impredicative_set c = impredicative_set := Declarations.ImpredicativeSet
-let type_in_type = ref Declarations.StratifiedType
-let set_type_in_type () = type_in_type := Declarations.TypeInType
+let set_type_in_type () =
+  let typing_flags = Environ.typing_flags (Global.env ()) in
+  Global.set_typing_flags { typing_flags with Declarations.check_universes = false }
 let engage () =
-  Global.set_engagement (!impredicative_set,!type_in_type)
+  Global.set_engagement !impredicative_set
 
 let set_batch_mode () = batch_mode := true
 
diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml
index 3d15f2142..4d8d537f2 100644
--- a/toplevel/obligations.ml
+++ b/toplevel/obligations.ml
@@ -567,7 +567,7 @@ let declare_mutual_definition l =
 	    List.map3 compute_possible_guardness_evidences
               wfl fixdefs fixtypes in
 	  let indexes = 
-              Pretyping.search_guard ~tflags:Declareops.safe_flags
+              Pretyping.search_guard
               Loc.ghost (Global.env())
               possible_indexes fixdecls in
           Some indexes, 
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 5131a4179..29d6d7acd 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -576,17 +576,17 @@ let vernac_inductive chk poly lo finite indl =
     let indl = List.map unpack indl in
     do_mutual_inductive chk indl poly lo finite
 
-let vernac_fixpoint ~flags locality poly local l =
+let vernac_fixpoint locality poly local l =
   let local = enforce_locality_exp locality local in
   if Dumpglob.dump () then
     List.iter (fun (((lid,_), _, _, _, _), _) -> Dumpglob.dump_definition lid false "def") l;
-  do_fixpoint ~flags local poly l
+  do_fixpoint local poly l
 
-let vernac_cofixpoint ~flags locality poly local l =
+let vernac_cofixpoint locality poly local l =
   let local = enforce_locality_exp locality local in
   if Dumpglob.dump () then
     List.iter (fun (((lid,_), _, _, _), _) -> Dumpglob.dump_definition lid false "def") l;
-  do_cofixpoint ~flags local poly l
+  do_cofixpoint local poly l
 
 let vernac_scheme l =
   if Dumpglob.dump () then
@@ -1731,8 +1731,6 @@ let vernac_load interp fname =
   try while true do interp (snd (parse_sentence input)) done
   with End_of_input -> ()
 
-let all_checks = Declareops.safe_flags
-
 (* "locality" is the prefix "Local" attribute, while the "local" component
  * is the outdated/deprecated "Local" attribute of some vernacular commands
  * still parsed as the obsolete_locality grammar entry for retrocompatibility.
@@ -1770,8 +1768,8 @@ let interp ?proof ~loc locality poly c =
   | VernacExactProof c -> vernac_exact_proof c
   | VernacAssumption (stre,nl,l) -> vernac_assumption locality poly stre l nl
   | VernacInductive (priv,finite,l) -> vernac_inductive true poly priv finite l
-  | VernacFixpoint (local, l) -> vernac_fixpoint locality ~flags:all_checks poly local l
-  | VernacCoFixpoint (local, l) -> vernac_cofixpoint ~flags:all_checks locality poly local l
+  | VernacFixpoint (local, l) -> vernac_fixpoint locality poly local l
+  | VernacCoFixpoint (local, l) -> vernac_cofixpoint locality poly local l
   | VernacScheme l -> vernac_scheme l
   | VernacCombinedScheme (id, l) -> vernac_combined_scheme id l
   | VernacUniverse l -> vernac_universe loc poly l