Merge PR #12586: [declare] Allow custom typing flags when declaring constants.

Reviewed-by: SkySkimmer
Reviewed-by: Zimmi48
Reviewed-by: gares
Reviewed-by: herbelin
Ack-by: jfehrle

15 files changed, 198 insertions, 94 deletions

diff --git a/vernac/attributes.ml b/vernac/attributes.ml
index fdaeedef8c..37895d22f5 100644
--- a/vernac/attributes.ml
+++ b/vernac/attributes.ml
@@ -338,3 +338,47 @@ let uses_parser : string key_parser = fun orig args ->
   |  _ -> CErrors.user_err (Pp.str "Ill formed \"using\" attribute")
 
 let using = attribute_of_list ["using",uses_parser]
+
+let process_typing_att ~typing_flags att disable =
+  let enable = not disable in
+  match att with
+  | "universes" ->
+    { typing_flags with
+      Declarations.check_universes = enable
+    }
+  | "guard" ->
+    { typing_flags with
+      Declarations.check_guarded = enable
+    }
+  | "positivity" ->
+    { typing_flags with
+      Declarations.check_positive = enable
+    }
+  | att ->
+    CErrors.user_err Pp.(str "Unknown “typing” attribute: " ++ str att)
+
+let process_typing_disable ~key = function
+  | VernacFlagEmpty | VernacFlagLeaf (FlagIdent "yes") ->
+    true
+  | VernacFlagLeaf (FlagIdent "no") ->
+    false
+  | _ ->
+    CErrors.user_err Pp.(str "Ill-formed attribute value, must be " ++ str key ++ str "={yes, no}")
+
+let typing_flags_parser : Declarations.typing_flags key_parser = fun orig args ->
+  let rec flag_parser typing_flags = function
+    | [] -> typing_flags
+    | (typing_att, enable) :: rest ->
+      let disable = process_typing_disable ~key:typing_att enable in
+      let typing_flags = process_typing_att ~typing_flags typing_att disable in
+      flag_parser typing_flags rest
+  in
+  match args with
+  | VernacFlagList atts ->
+    let typing_flags = Global.typing_flags () in
+    flag_parser typing_flags atts
+  | att ->
+    CErrors.user_err Pp.(str "Ill-formed “typing” attribute: " ++ pr_vernac_flag_value att)
+
+let typing_flags =
+  attribute_of_list ["bypass_check", typing_flags_parser]
diff --git a/vernac/attributes.mli b/vernac/attributes.mli
index 03a14a03ff..584e13e781 100644
--- a/vernac/attributes.mli
+++ b/vernac/attributes.mli
@@ -59,6 +59,9 @@ val canonical_field : bool attribute
 val canonical_instance : bool attribute
 val using : string option attribute
 
+(** Enable/Disable universe checking *)
+val typing_flags : Declarations.typing_flags option attribute
+
 val program_mode_option_name : string list
 (** For internal use when messing with the global option. *)
 
diff --git a/vernac/comDefinition.ml b/vernac/comDefinition.ml
index 81154bbea9..c54adb45f9 100644
--- a/vernac/comDefinition.ml
+++ b/vernac/comDefinition.ml
@@ -110,9 +110,10 @@ let interp_definition ~program_mode env evd impl_env bl red_option c ctypopt =
   let tyopt = Option.map (fun ty -> EConstr.it_mkProd_or_LetIn ty ctx) tyopt in
   evd, (c, tyopt), imps
 
-let do_definition ?hook ~name ~scope ~poly ~kind ?using udecl bl red_option c ctypopt =
+let do_definition ?hook ~name ~scope ~poly ?typing_flags ~kind ?using udecl bl red_option c ctypopt =
   let program_mode = false in
   let env = Global.env() in
+  let env = Environ.update_typing_flags ?typing_flags env in
   (* Explicitly bound universes and constraints *)
   let evd, udecl = interp_univ_decl_opt env udecl in
   let evd, (body, types), impargs =
@@ -125,14 +126,15 @@ let do_definition ?hook ~name ~scope ~poly ~kind ?using udecl bl red_option c ct
   in
   let kind = Decls.IsDefinition kind in
   let cinfo = Declare.CInfo.make ~name ~impargs ~typ:types ?using () in
-  let info = Declare.Info.make ~scope ~kind ?hook ~udecl ~poly () in
+  let info = Declare.Info.make ~scope ~kind ?hook ~udecl ~poly ?typing_flags () in
   let _ : Names.GlobRef.t =
     Declare.declare_definition ~info ~cinfo ~opaque:false ~body evd
   in ()
 
-let do_definition_program ?hook ~pm ~name ~scope ~poly ~kind ?using udecl bl red_option c ctypopt =
+let do_definition_program ?hook ~pm ~name ~scope ~poly ?typing_flags ~kind ?using udecl bl red_option c ctypopt =
   let program_mode = true in
   let env = Global.env() in
+  let env = Environ.update_typing_flags ?typing_flags env in
   (* Explicitly bound universes and constraints *)
   let evd, udecl = interp_univ_decl_opt env udecl in
   let evd, (body, types), impargs =
@@ -146,6 +148,6 @@ let do_definition_program ?hook ~pm ~name ~scope ~poly ~kind ?using udecl bl red
   let term, typ, uctx, obls = Declare.Obls.prepare_obligation ~name ~body ~types evd in
   let pm, _ =
     let cinfo = Declare.CInfo.make ~name ~typ ~impargs ?using () in
-    let info = Declare.Info.make ~udecl ~scope ~poly ~kind ?hook () in
+    let info = Declare.Info.make ~udecl ~scope ~poly ~kind ?hook ?typing_flags () in
     Declare.Obls.add_definition ~pm ~cinfo ~info ~term ~uctx obls
   in pm
diff --git a/vernac/comDefinition.mli b/vernac/comDefinition.mli
index 5e1b705ae4..9962e44098 100644
--- a/vernac/comDefinition.mli
+++ b/vernac/comDefinition.mli
@@ -30,6 +30,7 @@ val do_definition
   -> name:Id.t
   -> scope:Locality.locality
   -> poly:bool
+  -> ?typing_flags:Declarations.typing_flags
   -> kind:Decls.definition_object_kind
   -> ?using:Vernacexpr.section_subset_expr
   -> universe_decl_expr option
@@ -45,6 +46,7 @@ val do_definition_program
   -> name:Id.t
   -> scope:Locality.locality
   -> poly:bool
+  -> ?typing_flags:Declarations.typing_flags
   -> kind:Decls.logical_kind
   -> ?using:Vernacexpr.section_subset_expr
   -> universe_decl_expr option
diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml
index dd6c985bf9..0cf0b07822 100644
--- a/vernac/comFixpoint.ml
+++ b/vernac/comFixpoint.ml
@@ -158,10 +158,9 @@ type ('constr, 'types) recursive_preentry =
 let fix_proto sigma =
   Evarutil.new_global sigma (Coqlib.lib_ref "program.tactic.fix_proto")
 
-let interp_recursive ~program_mode ~cofix (fixl : 'a Vernacexpr.fix_expr_gen list) =
+let interp_recursive env ~program_mode ~cofix (fixl : 'a Vernacexpr.fix_expr_gen list) =
   let open Context.Named.Declaration in
   let open EConstr in
-  let env = Global.env() in
   let fixnames = List.map (fun fix -> fix.Vernacexpr.fname.CAst.v) fixl in
 
   (* Interp arities allowing for unresolved types *)
@@ -241,11 +240,13 @@ let ground_fixpoint env evd (fixnames,fixrs,fixdefs,fixtypes) =
   Evd.evar_universe_context evd, (fixnames,fixrs,fixdefs,fixtypes)
 
 (* XXX: Unify with interp_recursive  *)
-let interp_fixpoint ?(check_recursivity=true) ~cofix l :
+let interp_fixpoint ?(check_recursivity=true) ?typing_flags ~cofix l :
   ( (Constr.t, Constr.types) recursive_preentry *
     UState.universe_decl * UState.t *
     (EConstr.rel_context * Impargs.manual_implicits * int option) list) =
-  let (env,_,pl,evd),fix,info = interp_recursive ~program_mode:false ~cofix l in
+  let env = Global.env () in
+  let env = Environ.update_typing_flags ?typing_flags env in
+  let (env,_,pl,evd),fix,info = interp_recursive env ~program_mode:false ~cofix l in
   if check_recursivity then check_recursive true env evd fix;
   let evd = Pretyping.(solve_remaining_evars all_no_fail_flags env evd) in
   let uctx,fix = ground_fixpoint env evd fix in
@@ -271,12 +272,12 @@ let build_recthms ~indexes ?using fixnames fixtypes fiximps =
   in
   fix_kind, cofix, thms
 
-let declare_fixpoint_interactive_generic ?indexes ~scope ~poly ((fixnames,_fixrs,fixdefs,fixtypes),udecl,ctx,fiximps) ntns =
+let declare_fixpoint_interactive_generic ?indexes ~scope ~poly ?typing_flags ((fixnames,_fixrs,fixdefs,fixtypes),udecl,ctx,fiximps) ntns =
   let fix_kind, cofix, thms = build_recthms ~indexes fixnames fixtypes fiximps in
   let indexes = Option.default [] indexes in
   let init_terms = Some fixdefs in
   let evd = Evd.from_ctx ctx in
-  let info = Declare.Info.make ~poly ~scope ~kind:(Decls.IsDefinition fix_kind) ~udecl () in
+  let info = Declare.Info.make ~poly ~scope ~kind:(Decls.IsDefinition fix_kind) ~udecl ?typing_flags () in
   let lemma =
     Declare.Proof.start_mutual_with_initialization ~info
       evd ~mutual_info:(cofix,indexes,init_terms) ~cinfo:thms None in
@@ -284,13 +285,13 @@ let declare_fixpoint_interactive_generic ?indexes ~scope ~poly ((fixnames,_fixrs
   List.iter (Metasyntax.add_notation_interpretation (Global.env())) ntns;
   lemma
 
-let declare_fixpoint_generic ?indexes ~scope ~poly ?using ((fixnames,fixrs,fixdefs,fixtypes),udecl,uctx,fiximps) ntns =
+let declare_fixpoint_generic ?indexes ~scope ~poly ?typing_flags ?using ((fixnames,fixrs,fixdefs,fixtypes),udecl,uctx,fiximps) ntns =
   (* We shortcut the proof process *)
   let fix_kind, cofix, fixitems = build_recthms ~indexes ?using fixnames fixtypes fiximps in
   let fixdefs = List.map Option.get fixdefs in
   let rec_declaration = prepare_recursive_declaration fixnames fixrs fixtypes fixdefs in
   let fix_kind = Decls.IsDefinition fix_kind in
-  let info = Declare.Info.make ~scope ~kind:fix_kind ~poly ~udecl () in
+  let info = Declare.Info.make ~scope ~kind:fix_kind ~poly ~udecl ?typing_flags () in
   let cinfo = fixitems in
   let _ : GlobRef.t list =
     Declare.declare_mutually_recursive ~cinfo ~info ~opaque:false ~uctx
@@ -322,22 +323,22 @@ let adjust_rec_order ~structonly binders rec_order =
   in
   Option.map (extract_decreasing_argument ~structonly) rec_order
 
-let do_fixpoint_common (fixl : Vernacexpr.fixpoint_expr list) =
+let do_fixpoint_common ?typing_flags (fixl : Vernacexpr.fixpoint_expr list) =
   let fixl = List.map (fun fix ->
       Vernacexpr.{ fix
                    with rec_order = adjust_rec_order ~structonly:true fix.binders fix.rec_order }) fixl in
   let ntns = List.map_append (fun { Vernacexpr.notations } -> notations ) fixl in
-  let (_, _, _, info as fix) = interp_fixpoint ~cofix:false fixl in
+  let (_, _, _, info as fix) = interp_fixpoint ~cofix:false ?typing_flags fixl in
   fixl, ntns, fix, List.map compute_possible_guardness_evidences info
 
-let do_fixpoint_interactive ~scope ~poly l : Declare.Proof.t =
-  let fixl, ntns, fix, possible_indexes = do_fixpoint_common l in
-  let lemma = declare_fixpoint_interactive_generic ~indexes:possible_indexes ~scope ~poly fix ntns in
+let do_fixpoint_interactive ~scope ~poly ?typing_flags l : Declare.Proof.t =
+  let fixl, ntns, fix, possible_indexes = do_fixpoint_common ?typing_flags l in
+  let lemma = declare_fixpoint_interactive_generic ~indexes:possible_indexes ~scope ~poly ?typing_flags fix ntns in
   lemma
 
-let do_fixpoint ~scope ~poly ?using l =
-  let fixl, ntns, fix, possible_indexes = do_fixpoint_common l in
-  declare_fixpoint_generic ~indexes:possible_indexes ~scope ~poly ?using fix ntns
+let do_fixpoint ~scope ~poly ?typing_flags ?using l =
+  let fixl, ntns, fix, possible_indexes = do_fixpoint_common ?typing_flags l in
+  declare_fixpoint_generic ~indexes:possible_indexes ~scope ~poly ?typing_flags ?using fix ntns
 
 let do_cofixpoint_common (fixl : Vernacexpr.cofixpoint_expr list) =
   let fixl = List.map (fun fix -> {fix with Vernacexpr.rec_order = None}) fixl in
diff --git a/vernac/comFixpoint.mli b/vernac/comFixpoint.mli
index a36aba7672..faa5fce375 100644
--- a/vernac/comFixpoint.mli
+++ b/vernac/comFixpoint.mli
@@ -15,11 +15,20 @@ open Vernacexpr
 
 (** Entry points for the vernacular commands Fixpoint and CoFixpoint *)
 
-val do_fixpoint_interactive :
-  scope:Locality.locality -> poly:bool -> fixpoint_expr list -> Declare.Proof.t
+val do_fixpoint_interactive
+  : scope:Locality.locality
+  -> poly:bool
+  -> ?typing_flags:Declarations.typing_flags
+  -> fixpoint_expr list
+  -> Declare.Proof.t
 
-val do_fixpoint :
-  scope:Locality.locality -> poly:bool -> ?using:Vernacexpr.section_subset_expr -> fixpoint_expr list -> unit
+val do_fixpoint
+   : scope:Locality.locality
+  -> poly:bool
+  -> ?typing_flags:Declarations.typing_flags
+  -> ?using:Vernacexpr.section_subset_expr
+  -> fixpoint_expr list
+  -> unit
 
 val do_cofixpoint_interactive :
   scope:Locality.locality -> poly:bool -> cofixpoint_expr list -> Declare.Proof.t
@@ -44,6 +53,7 @@ type ('constr, 'types) recursive_preentry = Id.t list * Sorts.relevance list * '
 
 (** Exported for Program *)
 val interp_recursive :
+  Environ.env ->
   (* Misc arguments *)
   program_mode:bool -> cofix:bool ->
   (* Notations of the fixpoint / should that be folded in the previous argument? *)
@@ -58,8 +68,9 @@ val interp_recursive :
 (** Exported for Funind *)
 
 val interp_fixpoint
-  :  ?check_recursivity:bool ->
-     cofix:bool
+  :  ?check_recursivity:bool
+  -> ?typing_flags:Declarations.typing_flags
+  -> cofix:bool
   -> lident option fix_expr_gen list
   -> (Constr.t, Constr.types) recursive_preentry *
      UState.universe_decl * UState.t *
diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml
index 8cb077ca21..2be6097184 100644
--- a/vernac/comInductive.ml
+++ b/vernac/comInductive.ml
@@ -631,7 +631,7 @@ type uniform_inductive_flag =
   | UniformParameters
   | NonUniformParameters
 
-let do_mutual_inductive ~template udecl indl ~cumulative ~poly ~private_ind ~uniform finite =
+let do_mutual_inductive ~template udecl indl ~cumulative ~poly ?typing_flags ~private_ind ~uniform finite =
   let (params,indl),coes,ntns = extract_mutual_inductive_declaration_components indl in
   (* Interpret the types *)
   let indl = match params with
@@ -640,9 +640,11 @@ let do_mutual_inductive ~template udecl indl ~cumulative ~poly ~private_ind ~uni
       | UniformParameters -> (params, [], indl)
       | NonUniformParameters -> ([], params, indl)
   in
-  let mie,pl,impls = interp_mutual_inductive_gen (Global.env()) ~template udecl indl ntns ~cumulative ~poly ~private_ind finite in
+  let env = Global.env () in
+  let env = Environ.update_typing_flags ?typing_flags env in
+  let mie,pl,impls = interp_mutual_inductive_gen env ~template udecl indl ntns ~cumulative ~poly ~private_ind finite in
   (* Declare the mutual inductive block with its associated schemes *)
-  ignore (DeclareInd.declare_mutual_inductive_with_eliminations mie pl impls);
+  ignore (DeclareInd.declare_mutual_inductive_with_eliminations ?typing_flags mie pl impls);
   (* Declare the possible notations of inductive types *)
   List.iter (Metasyntax.add_notation_interpretation (Global.env ())) ntns;
   (* Declare the coercions *)
diff --git a/vernac/comInductive.mli b/vernac/comInductive.mli
index 8bce884ba4..e049bacb26 100644
--- a/vernac/comInductive.mli
+++ b/vernac/comInductive.mli
@@ -26,6 +26,7 @@ val do_mutual_inductive
   -> (one_inductive_expr * decl_notation list) list
   -> cumulative:bool
   -> poly:bool
+  -> ?typing_flags:Declarations.typing_flags
   -> private_ind:bool
   -> uniform:uniform_inductive_flag
   -> Declarations.recursivity_kind
diff --git a/vernac/comProgramFixpoint.ml b/vernac/comProgramFixpoint.ml
index 31f91979d3..3c4a651cf5 100644
--- a/vernac/comProgramFixpoint.ml
+++ b/vernac/comProgramFixpoint.ml
@@ -109,7 +109,7 @@ let telescope env sigma l =
 let nf_evar_context sigma ctx =
   List.map (map_constr (fun c -> Evarutil.nf_evar sigma c)) ctx
 
-let build_wellfounded pm (recname,pl,bl,arityc,body) poly ?using r measure notation =
+let build_wellfounded pm (recname,pl,bl,arityc,body) poly ?typing_flags ?using r measure notation =
   let open EConstr in
   let open Vars in
   let lift_rel_context n l = Termops.map_rel_context_with_binders (liftn n) l in
@@ -266,7 +266,7 @@ let build_wellfounded pm (recname,pl,bl,arityc,body) poly ?using r measure notat
   in
   let uctx = Evd.evar_universe_context sigma in
   let cinfo = Declare.CInfo.make ~name:recname ~typ:evars_typ ?using () in
-  let info = Declare.Info.make ~udecl ~poly ~hook () in
+  let info = Declare.Info.make ~udecl ~poly ~hook ?typing_flags () in
   let pm, _ =
     Declare.Obls.add_definition ~pm ~cinfo ~info ~term:evars_def ~uctx evars in
   pm
@@ -280,10 +280,12 @@ let collect_evars_of_term evd c ty =
   Evar.Set.fold (fun ev acc -> Evd.add acc ev (Evd.find_undefined evd ev))
   evars (Evd.from_ctx (Evd.evar_universe_context evd))
 
-let do_program_recursive ~pm ~scope ~poly ?using fixkind fixl =
+let do_program_recursive ~pm ~scope ~poly ?typing_flags ?using fixkind fixl =
   let cofix = fixkind = Declare.Obls.IsCoFixpoint in
   let (env, rec_sign, udecl, evd), fix, info =
-    interp_recursive ~cofix ~program_mode:true fixl
+    let env = Global.env () in
+    let env = Environ.update_typing_flags ?typing_flags env in
+    interp_recursive env ~cofix ~program_mode:true fixl
   in
     (* Program-specific code *)
     (* Get the interesting evars, those that were not instantiated *)
@@ -320,10 +322,13 @@ let do_program_recursive ~pm ~scope ~poly ?using fixkind fixl =
         Array.of_list (List.map (subst_vars (List.rev fixnames)) fixdefs)
       in
       let indexes =
-        Pretyping.search_guard (Global.env ()) possible_indexes fixdecls in
+        let env = Global.env () in
+        let env = Environ.update_typing_flags ?typing_flags env in
+        Pretyping.search_guard env possible_indexes fixdecls in
+      let env = Environ.update_typing_flags ?typing_flags env in
       List.iteri (fun i _ ->
           Inductive.check_fix env
-                              ((indexes,i),fixdecls))
+            ((indexes,i),fixdecls))
         fixl
   end in
   let uctx = Evd.evar_universe_context evd in
@@ -332,16 +337,16 @@ let do_program_recursive ~pm ~scope ~poly ?using fixkind fixl =
   | Declare.Obls.IsCoFixpoint -> Decls.(IsDefinition CoFixpoint)
   in
   let ntns = List.map_append (fun { Vernacexpr.notations } -> notations ) fixl in
-  let info = Declare.Info.make ~poly ~scope ~kind ~udecl () in
+  let info = Declare.Info.make ~poly ~scope ~kind ~udecl ?typing_flags () in
   Declare.Obls.add_mutual_definitions ~pm defs ~info ~uctx ~ntns fixkind
 
-let do_fixpoint ~pm ~scope ~poly ?using l =
+let do_fixpoint ~pm ~scope ~poly ?typing_flags ?using l =
   let g = List.map (fun { Vernacexpr.rec_order } -> rec_order) l in
     match g, l with
     | [Some { CAst.v = CWfRec (n,r) }],
       [ Vernacexpr.{fname={CAst.v=id}; univs; binders; rtype; body_def; notations} ] ->
         let recarg = mkIdentC n.CAst.v in
-        build_wellfounded pm (id, univs, binders, rtype, out_def body_def) poly ?using r recarg notations
+        build_wellfounded pm (id, univs, binders, rtype, out_def body_def) poly ?typing_flags ?using r recarg notations
 
     | [Some { CAst.v = CMeasureRec (n, m, r) }],
       [Vernacexpr.{fname={CAst.v=id}; univs; binders; rtype; body_def; notations }] ->
@@ -354,7 +359,7 @@ let do_fixpoint ~pm ~scope ~poly ?using l =
           user_err Pp.(str"Measure takes only two arguments in Program Fixpoint.")
         | _, _ -> r
       in
-        build_wellfounded pm (id, univs, binders, rtype, out_def body_def) poly ?using
+        build_wellfounded pm (id, univs, binders, rtype, out_def body_def) poly ?typing_flags ?using
           (Option.default (CAst.make @@ CRef (lt_ref,None)) r) m notations
 
     | _, _ when List.for_all (fun ro -> match ro with None | Some { CAst.v = CStructRec _} -> true | _ -> false) g ->
@@ -362,7 +367,7 @@ let do_fixpoint ~pm ~scope ~poly ?using l =
           Vernacexpr.(ComFixpoint.adjust_rec_order ~structonly:true fix.binders fix.rec_order)) l in
       let fixkind = Declare.Obls.IsFixpoint annots in
       let l = List.map2 (fun fix rec_order -> { fix with Vernacexpr.rec_order }) l annots in
-      do_program_recursive ~pm ~scope ~poly ?using fixkind l
+      do_program_recursive ~pm ~scope ~poly ?typing_flags ?using fixkind l
     | _, _ ->
       CErrors.user_err ~hdr:"do_fixpoint"
         (str "Well-founded fixpoints not allowed in mutually recursive blocks")
diff --git a/vernac/comProgramFixpoint.mli b/vernac/comProgramFixpoint.mli
index 30bf3ae8f8..0193be8683 100644
--- a/vernac/comProgramFixpoint.mli
+++ b/vernac/comProgramFixpoint.mli
@@ -15,6 +15,7 @@ val do_fixpoint :
      pm:Declare.OblState.t
   -> scope:Locality.locality
   -> poly:bool
+  -> ?typing_flags:Declarations.typing_flags
   -> ?using:Vernacexpr.section_subset_expr
   -> fixpoint_expr list
   -> Declare.OblState.t
diff --git a/vernac/declare.ml b/vernac/declare.ml
index 73ebca276d..fafee13bf6 100644
--- a/vernac/declare.ml
+++ b/vernac/declare.ml
@@ -83,14 +83,15 @@ module Info = struct
     ; udecl : UState.universe_decl
     ; scope : Locality.locality
     ; hook : Hook.t option
+    ; typing_flags : Declarations.typing_flags option
     }
 
   (** Note that [opaque] doesn't appear here as it is not known at the
      start of the proof in the interactive case. *)
   let make ?(poly=false) ?(inline=false) ?(kind=Decls.(IsDefinition Definition))
       ?(udecl=UState.default_univ_decl) ?(scope=Locality.Global Locality.ImportDefaultBehavior)
-      ?hook () =
-    { poly; inline; kind; udecl; scope; hook }
+      ?hook ?typing_flags () =
+    { poly; inline; kind; udecl; scope; hook; typing_flags }
 
 end
 
@@ -325,12 +326,12 @@ let cast_opaque_proof_entry (type a b) (entry : (a, b) effect_entry) (e : a proo
 
 let feedback_axiom () = Feedback.(feedback AddedAxiom)
 
-let is_unsafe_typing_flags () =
+let is_unsafe_typing_flags flags =
+  let flags = Option.default (Global.typing_flags ()) flags in
   let open Declarations in
-  let flags = Environ.typing_flags (Global.env()) in
   not (flags.check_universes && flags.check_guarded && flags.check_positive)
 
-let define_constant ~name cd =
+let define_constant ~name ~typing_flags cd =
   (* Logically define the constant and its subproofs, no libobject tampering *)
   let decl, unsafe = match cd with
     | DefinitionEntry de ->
@@ -354,13 +355,13 @@ let define_constant ~name cd =
     | PrimitiveEntry e ->
       ConstantEntry (Entries.PrimitiveEntry e), false
   in
-  let kn = Global.add_constant name decl in
-  if unsafe || is_unsafe_typing_flags() then feedback_axiom();
+  let kn = Global.add_constant ?typing_flags name decl in
+  if unsafe || is_unsafe_typing_flags typing_flags then feedback_axiom();
   kn
 
-let declare_constant ?(local = Locality.ImportDefaultBehavior) ~name ~kind cd =
+let declare_constant ?(local = Locality.ImportDefaultBehavior) ~name ~kind ~typing_flags cd =
   let () = check_exists name in
-  let kn = define_constant ~name cd in
+  let kn = define_constant ~typing_flags ~name cd in
   (* Register the libobjects attached to the constants *)
   let () = register_constant kn kind local in
   kn
@@ -557,7 +558,7 @@ let declare_definition_scheme ~internal ~univs ~role ~name c =
   kn, eff
 
 (* Locality stuff *)
-let declare_entry_core ~name ~scope ~kind ?hook ~obls ~impargs ~uctx entry =
+let declare_entry_core ~name ~scope ~kind ~typing_flags ?hook ~obls ~impargs ~uctx entry =
   let should_suggest =
     entry.proof_entry_opaque
     && not (List.is_empty (Global.named_context()))
@@ -570,7 +571,7 @@ let declare_entry_core ~name ~scope ~kind ?hook ~obls ~impargs ~uctx entry =
     if should_suggest then Proof_using.suggest_variable (Global.env ()) name;
     Names.GlobRef.VarRef name
   | Locality.Global local ->
-    let kn = declare_constant ~name ~local ~kind (DefinitionEntry entry) in
+    let kn = declare_constant ~name ~local ~kind ~typing_flags (DefinitionEntry entry) in
     let gr = Names.GlobRef.ConstRef kn in
     if should_suggest then Proof_using.suggest_constant (Global.env ()) kn;
     let () = DeclareUniv.declare_univ_binders gr ubind in
@@ -583,10 +584,11 @@ let declare_entry_core ~name ~scope ~kind ?hook ~obls ~impargs ~uctx entry =
 
 let declare_entry = declare_entry_core ~obls:[]
 
-let mutual_make_bodies ~fixitems ~rec_declaration ~possible_indexes =
+let mutual_make_bodies ~typing_flags ~fixitems ~rec_declaration ~possible_indexes =
   match possible_indexes with
   | Some possible_indexes ->
     let env = Global.env() in
+    let env = Environ.update_typing_flags ?typing_flags env in
     let indexes = Pretyping.search_guard env possible_indexes rec_declaration in
     let vars = Vars.universes_of_constr (Constr.mkFix ((indexes,0),rec_declaration)) in
     let fixdecls = CList.map_i (fun i _ -> Constr.mkFix ((indexes,i),rec_declaration)) 0 fixitems in
@@ -597,9 +599,9 @@ let mutual_make_bodies ~fixitems ~rec_declaration ~possible_indexes =
     vars, fixdecls, None
 
 let declare_mutually_recursive_core ~info ~cinfo ~opaque ~ntns ~uctx ~rec_declaration ~possible_indexes ?(restrict_ucontext=true) () =
-  let { Info.poly; udecl; scope; kind; _ } = info in
+  let { Info.poly; udecl; scope; kind; typing_flags; _ } = info in
   let vars, fixdecls, indexes =
-    mutual_make_bodies ~fixitems:cinfo ~rec_declaration ~possible_indexes in
+    mutual_make_bodies ~typing_flags ~fixitems:cinfo ~rec_declaration ~possible_indexes in
   let uctx, univs =
     (* XXX: Obligations don't do this, this seems like a bug? *)
     if restrict_ucontext
@@ -614,7 +616,7 @@ let declare_mutually_recursive_core ~info ~cinfo ~opaque ~ntns ~uctx ~rec_declar
   let csts = CList.map2
       (fun CInfo.{ name; typ; impargs; using } body ->
          let entry = definition_entry ~opaque ~types:typ ~univs ?using body in
-         declare_entry ~name ~scope ~kind ~impargs ~uctx entry)
+         declare_entry ~name ~scope ~kind ~impargs ~uctx ~typing_flags entry)
       cinfo fixdecls
   in
   let isfix = Option.has_some possible_indexes in
@@ -637,7 +639,7 @@ let declare_assumption ~name ~scope ~hook ~impargs ~uctx pe =
   in
   let kind = Decls.(IsAssumption Conjectural) in
   let decl = ParameterEntry pe in
-  let kn = declare_constant ~name ~local ~kind decl in
+  let kn = declare_constant ~name ~local ~kind ~typing_flags:None decl in
   let dref = Names.GlobRef.ConstRef kn in
   let () = Impargs.maybe_declare_manual_implicits false dref impargs in
   let () = assumption_message name in
@@ -680,8 +682,8 @@ let prepare_definition ~info ~opaque ?using ~body ~typ sigma =
 let declare_definition_core ~info ~cinfo ~opaque ~obls ~body sigma =
   let { CInfo.name; impargs; typ; using; _ } = cinfo in
   let entry, uctx = prepare_definition ~info ~opaque ?using ~body ~typ sigma in
-  let { Info.scope; kind; hook; _ } = info in
-  declare_entry_core ~name ~scope ~kind ~impargs ~obls ?hook ~uctx entry, uctx
+  let { Info.scope; kind; hook; typing_flags; _ } = info in
+  declare_entry_core ~name ~scope ~kind ~impargs ~typing_flags ~obls ?hook ~uctx entry, uctx
 
 let declare_definition ~info ~cinfo ~opaque ~body sigma =
   declare_definition_core ~obls:[] ~info ~cinfo ~opaque ~body sigma |> fst
@@ -913,6 +915,7 @@ let declare_obligation prg obl ~uctx ~types ~body =
     (* ppedrot: seems legit to have obligations as local *)
     let constant =
       declare_constant ~name:obl.obl_name
+        ~typing_flags:prg.prg_info.Info.typing_flags
         ~local:Locality.ImportNeedQualified
         ~kind:Decls.(IsProof Property)
         (DefinitionEntry ce)
@@ -1425,9 +1428,9 @@ let start_proof_core ~name ~typ ~pinfo ?(sign=initialize_named_context_for_proof
      marked "opaque", this is a hack tho, see #10446, and
      build_constant_by_tactic uses a different method that would break
      program_inference_hook *)
-  let { Proof_info.info = { Info.poly; _ }; _ } = pinfo in
+  let { Proof_info.info = { Info.poly; typing_flags; _ }; _ } = pinfo in
   let goals = [Global.env_of_context sign, typ] in
-  let proof = Proof.start ~name ~poly sigma goals in
+  let proof = Proof.start ~name ~poly ?typing_flags sigma goals in
   let initial_euctx = Evd.evar_universe_context Proof.((data proof).sigma) in
   { proof
   ; endline_tactic = None
@@ -1448,7 +1451,8 @@ let start_core ~info ~cinfo ?proof_ending sigma =
 let start = start_core ?proof_ending:None
 
 let start_dependent ~info ~name ~proof_ending goals =
-  let proof = Proof.dependent_start ~name ~poly:info.Info.poly goals in
+  let { Info.poly; typing_flags; _ } = info in
+  let proof = Proof.dependent_start ~name ~poly ?typing_flags goals in
   let initial_euctx = Evd.evar_universe_context Proof.((data proof).sigma) in
   let cinfo = [] in
   let pinfo = Proof_info.make ~info ~cinfo ~proof_ending () in
@@ -1886,7 +1890,7 @@ end = struct
 
   let declare_mutdef ~uctx ~pinfo pe i CInfo.{ name; impargs; typ; _} =
     let { Proof_info.info; compute_guard; _ } = pinfo in
-    let { Info.hook; scope; kind; _ } = info in
+    let { Info.hook; scope; kind; typing_flags; _ } = info in
     (* if i = 0 , we don't touch the type; this is for compat
        but not clear it is the right thing to do.
     *)
@@ -1903,7 +1907,7 @@ end = struct
         Internal.map_entry_body pe
           ~f:(fun ((body, ctx), eff) -> (select_body i body, ctx), eff)
     in
-    declare_entry ~name ~scope ~kind ?hook ~impargs ~uctx pe
+    declare_entry ~name ~scope ~kind ?hook ~impargs ~typing_flags ~uctx pe
 
   let declare_mutdef ~pinfo ~uctx ~entry =
     let pe = match pinfo.Proof_info.compute_guard with
@@ -1913,6 +1917,8 @@ end = struct
     | possible_indexes ->
       (* Try all combinations... not optimal *)
       let env = Global.env() in
+      let typing_flags = pinfo.Proof_info.info.Info.typing_flags in
+      let env = Environ.update_typing_flags ?typing_flags env in
       Internal.map_entry_body entry
         ~f:(guess_decreasing env possible_indexes)
     in
@@ -1993,7 +1999,7 @@ let finish_derived ~f ~name ~entries =
   let f_def = Internal.set_opacity ~opaque:false f_def in
   let f_kind = Decls.(IsDefinition Definition) in
   let f_def = DefinitionEntry f_def in
-  let f_kn = declare_constant ~name:f ~kind:f_kind f_def in
+  let f_kn = declare_constant ~name:f ~kind:f_kind f_def ~typing_flags:None in
   let f_kn_term = Constr.mkConst f_kn in
   (* In the type and body of the proof of [suchthat] there can be
      references to the variable [f]. It needs to be replaced by
@@ -2011,7 +2017,7 @@ let finish_derived ~f ~name ~entries =
   (* The same is done in the body of the proof. *)
   let lemma_def = Internal.map_entry_body lemma_def ~f:(fun ((b,ctx),fx) -> (substf b, ctx), fx) in
   let lemma_def = DefinitionEntry lemma_def in
-  let ct = declare_constant ~name ~kind:Decls.(IsProof Proposition) lemma_def in
+  let ct = declare_constant ~name ~typing_flags:None ~kind:Decls.(IsProof Proposition) lemma_def in
   [GlobRef.ConstRef f_kn; GlobRef.ConstRef ct]
 
 let finish_proved_equations ~pm ~kind ~hook i proof_obj types sigma0 =
@@ -2025,7 +2031,7 @@ let finish_proved_equations ~pm ~kind ~hook i proof_obj types sigma0 =
           | None -> let n = !obls in incr obls; Nameops.add_suffix i ("_obligation_" ^ string_of_int n)
         in
         let entry, args = Internal.shrink_entry local_context entry in
-        let cst = declare_constant ~name:id ~kind (DefinitionEntry entry) in
+        let cst = declare_constant ~name:id ~kind ~typing_flags:None (DefinitionEntry entry) in
         let sigma, app = Evarutil.new_global sigma (GlobRef.ConstRef cst) in
         let sigma = Evd.define ev (EConstr.applist (app, List.map EConstr.of_constr args)) sigma in
         sigma, cst) sigma0
@@ -2519,3 +2525,9 @@ type nonrec progress = progress =
 end
 
 module OblState = Obls_.State
+
+let declare_constant ?local ~name ~kind ?typing_flags =
+  declare_constant ?local ~name ~kind ~typing_flags
+
+let declare_entry ~name ~scope ~kind =
+  declare_entry ~name ~scope ~kind ~typing_flags:None
diff --git a/vernac/declare.mli b/vernac/declare.mli
index e4c77113af..37a61cc4f0 100644
--- a/vernac/declare.mli
+++ b/vernac/declare.mli
@@ -109,6 +109,7 @@ module Info : sig
     (** locality  *)
     -> ?hook : Hook.t
     (** Callback to be executed after saving the constant *)
+    -> ?typing_flags:Declarations.typing_flags
     -> unit
     -> t
 
@@ -387,6 +388,7 @@ val declare_constant
   :  ?local:Locality.import_status
   -> name:Id.t
   -> kind:Decls.logical_kind
+  -> ?typing_flags:Declarations.typing_flags
   -> Evd.side_effects constant_entry
   -> Constant.t
 
diff --git a/vernac/declareInd.ml b/vernac/declareInd.ml
index e22d63b811..7050ddc042 100644
--- a/vernac/declareInd.ml
+++ b/vernac/declareInd.ml
@@ -104,7 +104,7 @@ let is_unsafe_typing_flags () =
   not (flags.check_universes && flags.check_guarded && flags.check_positive)
 
 (* for initial declaration *)
-let declare_mind mie =
+let declare_mind ?typing_flags mie =
   let id = match mie.mind_entry_inds with
     | ind::_ -> ind.mind_entry_typename
     | [] -> CErrors.anomaly (Pp.str "cannot declare an empty list of inductives.") in
@@ -113,7 +113,7 @@ let declare_mind mie =
   List.iter (fun (typ, cons) ->
       Declare.check_exists typ;
       List.iter Declare.check_exists cons) names;
-  let _kn' = Global.add_mind id mie in
+  let _kn' = Global.add_mind ?typing_flags id mie in
   let (sp,kn as oname) = Lib.add_leaf id (inInductive { ind_names = names }) in
   if is_unsafe_typing_flags() then feedback_axiom ();
   let mind = Global.mind_of_delta_kn kn in
@@ -154,7 +154,7 @@ type one_inductive_impls =
   Impargs.manual_implicits (* for inds *) *
   Impargs.manual_implicits list (* for constrs *)
 
-let declare_mutual_inductive_with_eliminations ?(primitive_expected=false) mie pl impls =
+let declare_mutual_inductive_with_eliminations ?(primitive_expected=false) ?typing_flags mie pl impls =
   (* spiwack: raises an error if the structure is supposed to be non-recursive,
         but isn't *)
   begin match mie.mind_entry_finite with
@@ -166,7 +166,7 @@ let declare_mutual_inductive_with_eliminations ?(primitive_expected=false) mie p
     | _ -> ()
   end;
   let names = List.map (fun e -> e.mind_entry_typename) mie.mind_entry_inds in
-  let (_, kn), prim = declare_mind mie in
+  let (_, kn), prim = declare_mind ?typing_flags mie in
   let mind = Global.mind_of_delta_kn kn in
   if primitive_expected && not prim then warn_non_primitive_record (mind,0);
   DeclareUniv.declare_univ_binders (GlobRef.IndRef (mind,0)) pl;
diff --git a/vernac/declareInd.mli b/vernac/declareInd.mli
index 05a1617329..eacf20e30c 100644
--- a/vernac/declareInd.mli
+++ b/vernac/declareInd.mli
@@ -17,6 +17,7 @@ type one_inductive_impls =
 
 val declare_mutual_inductive_with_eliminations
   : ?primitive_expected:bool
+  -> ?typing_flags:Declarations.typing_flags
   -> Entries.mutual_inductive_entry
   -> UnivNames.universe_binders
   -> one_inductive_impls list
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 57b264bbc2..a3726daf63 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -57,16 +57,17 @@ module DefAttributes = struct
     program : bool;
     deprecated : Deprecation.t option;
     canonical_instance : bool;
+    typing_flags : Declarations.typing_flags option;
     using : Vernacexpr.section_subset_expr option;
   }
 
   let parse f =
     let open Attributes in
-    let ((((locality, deprecated), polymorphic), program), canonical_instance), using =
-      parse Notations.(locality ++ deprecation ++ polymorphic ++ program ++ canonical_instance ++ using) f
+    let (((((locality, deprecated), polymorphic), program), canonical_instance), typing_flags), using =
+      parse Notations.(locality ++ deprecation ++ polymorphic ++ program ++ canonical_instance ++ typing_flags ++ using) f
     in
     let using = Option.map Proof_using.using_from_string using in
-    { polymorphic; program; locality; deprecated; canonical_instance; using }
+    { polymorphic; program; locality; deprecated; canonical_instance; typing_flags; using }
 end
 
 let module_locality = Attributes.Notations.(locality >>= fun l -> return (make_module_locality l))
@@ -512,6 +513,7 @@ let vernac_set_used_variables ~pstate e : Declare.Proof.t =
     l;
   let _, pstate = Declare.Proof.set_used_variables pstate l in
   pstate
+
 let vernac_set_used_variables_opt ?using pstate =
   match using with
   | None -> pstate
@@ -546,28 +548,29 @@ let post_check_evd ~udecl ~poly evd =
   else (* We fix the variables to ensure they won't be lowered to Set *)
     Evd.fix_undefined_variables evd
 
-let start_lemma_com ~program_mode ~poly ~scope ~kind ?using ?hook thms =
+let start_lemma_com ~typing_flags ~program_mode ~poly ~scope ~kind ?using ?hook thms =
   let env0 = Global.env () in
+  let env0 = Environ.update_typing_flags ?typing_flags env0 in
   let flags = Pretyping.{ all_no_fail_flags with program_mode } in
   let decl = fst (List.hd thms) in
   let evd, udecl = Constrintern.interp_univ_decl_opt env0 (snd decl) in
   let evd, thms = interp_lemma ~program_mode ~flags ~scope env0 evd thms in
   let mut_analysis = RecLemmas.look_for_possibly_mutual_statements evd thms in
   let evd = Evd.minimize_universes evd in
-  let pstate =
+  let info = Declare.Info.make ?hook ~poly ~scope ~kind ~udecl ?typing_flags () in
+  begin
     match mut_analysis with
     | RecLemmas.NonMutual thm ->
       let thm = Declare.CInfo.to_constr evd thm in
       let evd = post_check_evd ~udecl ~poly evd in
-      let info = Declare.Info.make ?hook ~poly ~scope ~kind ~udecl () in
       Declare.Proof.start_with_initialization ~info ~cinfo:thm evd
     | RecLemmas.Mutual { mutual_info; cinfo ; possible_guards } ->
       let cinfo = List.map (Declare.CInfo.to_constr evd) cinfo in
       let evd = post_check_evd ~udecl ~poly evd in
-      let info = Declare.Info.make ?hook ~poly ~scope ~kind ~udecl () in
       Declare.Proof.start_mutual_with_initialization ~info ~cinfo evd ~mutual_info (Some possible_guards)
-  in
-  vernac_set_used_variables_opt ?using pstate
+  end
+  (* XXX: This should be handled in start_with_initialization, see duplicate using in declare.ml *)
+  |> vernac_set_used_variables_opt ?using
 
 let vernac_definition_hook ~canonical_instance ~local ~poly = let open Decls in function
 | Coercion ->
@@ -606,14 +609,16 @@ let vernac_definition_interactive ~atts (discharge, kind) (lid, pl) bl t =
   let hook = vernac_definition_hook ~canonical_instance:atts.canonical_instance ~local:atts.locality ~poly:atts.polymorphic kind in
   let program_mode = atts.program in
   let poly = atts.polymorphic in
+  let typing_flags = atts.typing_flags in
   let name = vernac_definition_name lid local in
-  start_lemma_com ~program_mode ~poly ~scope:local ~kind:(Decls.IsDefinition kind) ?using:atts.using ?hook [(name, pl), (bl, t)]
+  start_lemma_com ~typing_flags ~program_mode ~poly ~scope:local ~kind:(Decls.IsDefinition kind) ?using:atts.using ?hook [(name, pl), (bl, t)]
 
 let vernac_definition ~atts ~pm (discharge, kind) (lid, pl) bl red_option c typ_opt =
   let open DefAttributes in
   let scope = enforce_locality_exp atts.locality discharge in
   let hook = vernac_definition_hook ~canonical_instance:atts.canonical_instance ~local:atts.locality ~poly:atts.polymorphic kind in
   let program_mode = atts.program in
+  let typing_flags = atts.typing_flags in
   let name = vernac_definition_name lid scope in
   let red_option = match red_option with
     | None -> None
@@ -624,11 +629,11 @@ let vernac_definition ~atts ~pm (discharge, kind) (lid, pl) bl red_option c typ_
   if program_mode then
     let kind = Decls.IsDefinition kind in
     ComDefinition.do_definition_program ~pm ~name:name.v
-      ~poly:atts.polymorphic ~scope ~kind pl bl red_option c typ_opt ?hook
+      ~poly:atts.polymorphic ?typing_flags ~scope ~kind pl bl red_option c typ_opt ?hook
   else
     let () =
       ComDefinition.do_definition ~name:name.v
-        ~poly:atts.polymorphic ~scope ~kind ?using:atts.using pl bl red_option c typ_opt ?hook in
+        ~poly:atts.polymorphic ?typing_flags ~scope ~kind ?using:atts.using pl bl red_option c typ_opt ?hook in
     pm
 
 (* NB: pstate argument to use combinators easily *)
@@ -637,7 +642,11 @@ let vernac_start_proof ~atts kind l =
   let scope = enforce_locality_exp atts.locality NoDischarge in
   if Dumpglob.dump () then
     List.iter (fun ((id, _), _) -> Dumpglob.dump_definition id false "prf") l;
-  start_lemma_com ~program_mode:atts.program ~poly:atts.polymorphic ~scope ~kind:(Decls.IsProof kind) ?using:atts.using l
+  start_lemma_com
+    ~typing_flags:atts.typing_flags
+    ~program_mode:atts.program
+    ~poly:atts.polymorphic
+    ~scope ~kind:(Decls.IsProof kind) ?using:atts.using l
 
 let vernac_end_proof ~lemma ~pm = let open Vernacexpr in function
   | Admitted ->
@@ -720,7 +729,7 @@ let should_treat_as_uniform () =
   then ComInductive.UniformParameters
   else ComInductive.NonUniformParameters
 
-let vernac_record ~template udecl ~cumulative k ~poly finite records =
+let vernac_record ~template udecl ~cumulative k ~poly ?typing_flags finite records =
   let map ((is_coercion, name), binders, sort, nameopt, cfs) =
     let idbuild = match nameopt with
     | None -> Nameops.add_prefix "Build_" name.v
@@ -741,7 +750,13 @@ let vernac_record ~template udecl ~cumulative k ~poly finite records =
     Record.Ast.{ name; is_coercion; binders; cfs; idbuild; sort }
   in
   let records = List.map map records in
-  ignore(Record.definition_structure ~template udecl k ~cumulative ~poly finite records)
+  match typing_flags with
+  | Some _ ->
+    CErrors.user_err (Pp.str "typing flags are not yet supported for records")
+  | None ->
+    let _ : _ list =
+      Record.definition_structure ~template udecl k ~cumulative ~poly finite records in
+    ()
 
 let extract_inductive_udecl (indl:(inductive_expr * decl_notation list) list) =
   match indl with
@@ -773,8 +788,8 @@ let private_ind =
   | None -> return false
 
 let vernac_inductive ~atts kind indl =
-  let (template, (poly, cumulative)), private_ind = Attributes.(
-      parse Notations.(template ++ polymorphic_cumulative ++ private_ind) atts) in
+  let ((template, (poly, cumulative)), private_ind), typing_flags = Attributes.(
+      parse Notations.(template ++ polymorphic_cumulative ++ private_ind ++ typing_flags) atts) in
   let open Pp in
   let udecl, indl = extract_inductive_udecl indl in
   if Dumpglob.dump () then
@@ -811,7 +826,7 @@ let vernac_inductive ~atts kind indl =
     let coe' = if coe then BackInstance else NoInstance in
     let f = AssumExpr ((make ?loc:lid.loc @@ Name lid.v), [], ce),
             { rf_subclass = coe' ; rf_priority = None ; rf_notation = [] ; rf_canonical = true } in
-    vernac_record ~template udecl ~cumulative (Class true) ~poly finite [id, bl, c, None, [f]]
+    vernac_record ~template udecl ~cumulative (Class true) ~poly ?typing_flags finite [id, bl, c, None, [f]]
   else if List.for_all is_record indl then
     (* Mutual record case *)
     let () = match kind with
@@ -836,7 +851,7 @@ let vernac_inductive ~atts kind indl =
     in
     let kind = match kind with Class _ -> Class false | _ -> kind in
     let recordl = List.map unpack indl in
-    vernac_record ~template udecl ~cumulative kind ~poly finite recordl
+    vernac_record ~template udecl ~cumulative kind ~poly ?typing_flags finite recordl
   else if List.for_all is_constructor indl then
     (* Mutual inductive case *)
     let () = match kind with
@@ -860,7 +875,7 @@ let vernac_inductive ~atts kind indl =
     in
     let indl = List.map unpack indl in
     let uniform = should_treat_as_uniform () in
-    ComInductive.do_mutual_inductive ~template udecl indl ~cumulative ~poly ~private_ind ~uniform finite
+    ComInductive.do_mutual_inductive ~template udecl indl ~cumulative ~poly ?typing_flags ~private_ind ~uniform finite
   else
     user_err (str "Mixed record-inductive definitions are not allowed")
 
@@ -874,17 +889,19 @@ let vernac_fixpoint_interactive ~atts discharge l =
   let scope = vernac_fixpoint_common ~atts discharge l in
   if atts.program then
     CErrors.user_err Pp.(str"Program Fixpoint requires a body");
-  vernac_set_used_variables_opt ?using:atts.using
-    (ComFixpoint.do_fixpoint_interactive ~scope ~poly:atts.polymorphic l)
+  let typing_flags = atts.typing_flags in
+  ComFixpoint.do_fixpoint_interactive ~scope ~poly:atts.polymorphic ?typing_flags l
+  |> vernac_set_used_variables_opt ?using:atts.using
 
 let vernac_fixpoint ~atts ~pm discharge l =
   let open DefAttributes in
   let scope = vernac_fixpoint_common ~atts discharge l in
+  let typing_flags = atts.typing_flags in
   if atts.program then
     (* XXX: Switch to the attribute system and match on ~atts *)
-    ComProgramFixpoint.do_fixpoint ~pm ~scope ~poly:atts.polymorphic ?using:atts.using l
+    ComProgramFixpoint.do_fixpoint ~pm ~scope ~poly:atts.polymorphic ?typing_flags ?using:atts.using l
   else
-    let () = ComFixpoint.do_fixpoint ~scope ~poly:atts.polymorphic ?using:atts.using l in
+    let () = ComFixpoint.do_fixpoint ~scope ~poly:atts.polymorphic ?typing_flags ?using:atts.using l in
     pm
 
 let vernac_cofixpoint_common ~atts discharge l =