From b531ef305a0dad301629cf9a51a1a4f0ff925297 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Tue, 23 Jun 2020 22:51:23 +0200
Subject: [declare] Allow custom typing flags when declaring constants.

We use the new `Declare.Info` structure to uniformly add properties to
the handling of constants. In this case, per-constant typing flags.

The internal code may want to see some further refactoring, including
pushing the flags down to `Safe_typing.add_constant` , but the changes
in the interface should be definitive.

This will allow #12539 and #9004 using attributes.
---
 .../12-misc/12586-declare+typing_flags.rst         |  5 ++
 vernac/declare.ml                                  | 66 ++++++++++++++--------
 vernac/declare.mli                                 |  2 +
 3 files changed, 51 insertions(+), 22 deletions(-)
 create mode 100644 doc/changelog/12-misc/12586-declare+typing_flags.rst

diff --git a/doc/changelog/12-misc/12586-declare+typing_flags.rst b/doc/changelog/12-misc/12586-declare+typing_flags.rst
new file mode 100644
index 0000000000..001cd600b0
--- /dev/null
+++ b/doc/changelog/12-misc/12586-declare+typing_flags.rst
@@ -0,0 +1,5 @@
+- **Added:**
+  Typing flags can now be specified per-constant, this does allow
+  to fine-grain specify them from plugins or attributes.
+  (`#12586 <https://github.com/coq/coq/pull/12586>`_,
+  by Emilio Jesus Gallego Arias).
diff --git a/vernac/declare.ml b/vernac/declare.ml
index 73ebca276d..0b3b3aeb43 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,28 @@ 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 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 =
+(* Maybe it would make sense to push this logic down to
+   Safe_typing.add_constant? *)
+let add_constant_with_flags ~typing_flags ~unsafe ~name decl =
+  let current_flags = Global.typing_flags () in
+  let typing_flags = Option.cata
+      (fun new_flags -> Global.set_typing_flags new_flags; new_flags)
+      current_flags typing_flags in
+  try
+    let kn = Global.add_constant name decl in
+    Global.set_typing_flags current_flags;
+    if unsafe || is_unsafe_typing_flags typing_flags then feedback_axiom();
+    kn
+  with exn ->
+    let ie = Exninfo.capture exn in
+    Global.set_typing_flags current_flags;
+    Exninfo.iraise ie
+
+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 +371,11 @@ 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();
-  kn
+  add_constant_with_flags ~unsafe ~typing_flags ~name decl
 
-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 +572,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 +585,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
@@ -597,7 +612,7 @@ 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
   let uctx, univs =
@@ -614,7 +629,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 +652,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 +695,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 +928,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)
@@ -1886,7 +1902,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 +1919,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
@@ -1993,7 +2009,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 +2027,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 +2041,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 +2535,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
 
-- 
cgit v1.2.3


From b78f6424d9fa5a8027c4acb21b3e57ee6294bc5f Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Thu, 25 Jun 2020 16:43:08 +0200
Subject: [kernel] Allow to set typing flags in add_constant

This is just an experiment, but makes the uses of the API easier as we
don't mess with the global state anymore.
---
 kernel/safe_typing.ml  | 12 ++++++++++++
 kernel/safe_typing.mli |  1 +
 library/global.ml      |  2 +-
 library/global.mli     |  1 +
 vernac/declare.ml      | 22 ++++------------------
 5 files changed, 19 insertions(+), 19 deletions(-)

diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 6abd283f6c..1ecb5cba7d 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -247,6 +247,15 @@ let set_native_compiler b senv =
 
 let set_allow_sprop b senv = { senv with env = Environ.set_allow_sprop b senv.env }
 
+(* Temporary sets custom typing flags *)
+let with_typing_flags ?typing_flags senv ~f =
+  match typing_flags with
+  | None -> f senv
+  | Some typing_flags ->
+    let orig_typing_flags = Environ.typing_flags senv.env in
+    let res, senv = f (set_typing_flags typing_flags senv) in
+    res, set_typing_flags orig_typing_flags senv
+
 (** Check that the engagement [c] expected by a library matches
     the current (initial) one *)
 let check_engagement env expected_impredicative_set =
@@ -928,6 +937,9 @@ let add_constant l decl senv =
   in
   kn, senv
 
+let add_constant ?typing_flags l decl senv =
+  with_typing_flags ?typing_flags senv ~f:(add_constant l decl)
+
 let add_private_constant l decl senv : (Constant.t * private_constants) * safe_environment =
   let kn = Constant.make2 senv.modpath l in
     let cb =
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index 6fa9022906..c4d0fffe2b 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -93,6 +93,7 @@ val export_private_constants :
 
 (** returns the main constant *)
 val add_constant :
+  ?typing_flags:Declarations.typing_flags ->
   Label.t -> global_declaration -> Constant.t safe_transformer
 
 (** Similar to add_constant but also returns a certificate *)
diff --git a/library/global.ml b/library/global.ml
index 5c847fda96..238b9d554b 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -105,7 +105,7 @@ let is_cumulative_sprop () = (typing_flags()).Declarations.cumulative_sprop
 let set_allow_sprop b = globalize0 (Safe_typing.set_allow_sprop b)
 let sprop_allowed () = Environ.sprop_allowed (env())
 let export_private_constants cd = globalize (Safe_typing.export_private_constants cd)
-let add_constant id d = globalize (Safe_typing.add_constant (i2l id) d)
+let add_constant ?typing_flags id d = globalize (Safe_typing.add_constant ?typing_flags (i2l id) d)
 let add_private_constant id d = globalize (Safe_typing.add_private_constant (i2l id) d)
 let add_mind id mie = globalize (Safe_typing.add_mind (i2l id) mie)
 let add_modtype id me inl = globalize (Safe_typing.add_modtype (i2l id) me inl)
diff --git a/library/global.mli b/library/global.mli
index 5faf0e8bbd..4c2d427925 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -52,6 +52,7 @@ val export_private_constants :
   Safe_typing.exported_private_constant list
 
 val add_constant :
+  ?typing_flags:Declarations.typing_flags ->
   Id.t -> Safe_typing.global_declaration -> Constant.t
 val add_private_constant :
   Id.t -> Safe_typing.side_effect_declaration -> Constant.t * Safe_typing.private_constants
diff --git a/vernac/declare.ml b/vernac/declare.ml
index 0b3b3aeb43..210007d17d 100644
--- a/vernac/declare.ml
+++ b/vernac/declare.ml
@@ -327,26 +327,10 @@ 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 flags =
+  let flags = Option.default (Global.typing_flags ()) flags in
   let open Declarations in
   not (flags.check_universes && flags.check_guarded && flags.check_positive)
 
-(* Maybe it would make sense to push this logic down to
-   Safe_typing.add_constant? *)
-let add_constant_with_flags ~typing_flags ~unsafe ~name decl =
-  let current_flags = Global.typing_flags () in
-  let typing_flags = Option.cata
-      (fun new_flags -> Global.set_typing_flags new_flags; new_flags)
-      current_flags typing_flags in
-  try
-    let kn = Global.add_constant name decl in
-    Global.set_typing_flags current_flags;
-    if unsafe || is_unsafe_typing_flags typing_flags then feedback_axiom();
-    kn
-  with exn ->
-    let ie = Exninfo.capture exn in
-    Global.set_typing_flags current_flags;
-    Exninfo.iraise ie
-
 let define_constant ~name ~typing_flags cd =
   (* Logically define the constant and its subproofs, no libobject tampering *)
   let decl, unsafe = match cd with
@@ -371,7 +355,9 @@ let define_constant ~name ~typing_flags cd =
     | PrimitiveEntry e ->
       ConstantEntry (Entries.PrimitiveEntry e), false
   in
-  add_constant_with_flags ~unsafe ~typing_flags ~name decl
+  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 ~typing_flags cd =
   let () = check_exists name in
-- 
cgit v1.2.3


From 5a9e90e426ba2e25cbcb76af2bb67717984e2b6b Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Thu, 15 Oct 2020 16:48:38 +0200
Subject: [kernel] Allow to set typing flags in add_mind [inductive]

---
 kernel/safe_typing.ml  | 3 +++
 kernel/safe_typing.mli | 1 +
 library/global.ml      | 2 +-
 library/global.mli     | 1 +
 4 files changed, 6 insertions(+), 1 deletion(-)

diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 1ecb5cba7d..a35f94e3ce 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -995,6 +995,9 @@ let add_mind l mie senv =
   let mib = Indtypes.check_inductive senv.env ~sec_univs kn mie in
   kn, add_checked_mind kn mib senv
 
+let add_mind ?typing_flags l mie senv =
+  with_typing_flags ?typing_flags senv ~f:(add_mind l mie)
+
 (** Insertion of module types *)
 
 let add_modtype l params_mte inl senv =
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index c4d0fffe2b..287274e39a 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -103,6 +103,7 @@ val add_private_constant :
 (** Adding an inductive type *)
 
 val add_mind :
+  ?typing_flags:Declarations.typing_flags ->
   Label.t -> Entries.mutual_inductive_entry ->
     MutInd.t safe_transformer
 
diff --git a/library/global.ml b/library/global.ml
index 238b9d554b..71cadb3600 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -107,7 +107,7 @@ let sprop_allowed () = Environ.sprop_allowed (env())
 let export_private_constants cd = globalize (Safe_typing.export_private_constants cd)
 let add_constant ?typing_flags id d = globalize (Safe_typing.add_constant ?typing_flags (i2l id) d)
 let add_private_constant id d = globalize (Safe_typing.add_private_constant (i2l id) d)
-let add_mind id mie = globalize (Safe_typing.add_mind (i2l id) mie)
+let add_mind ?typing_flags id mie = globalize (Safe_typing.add_mind ?typing_flags (i2l id) mie)
 let add_modtype id me inl = globalize (Safe_typing.add_modtype (i2l id) me inl)
 let add_module id me inl = globalize (Safe_typing.add_module (i2l id) me inl)
 let add_include me ismod inl = globalize (Safe_typing.add_include me ismod inl)
diff --git a/library/global.mli b/library/global.mli
index 4c2d427925..c9b9d7f536 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -57,6 +57,7 @@ val add_constant :
 val add_private_constant :
   Id.t -> Safe_typing.side_effect_declaration -> Constant.t * Safe_typing.private_constants
 val add_mind :
+  ?typing_flags:Declarations.typing_flags ->
   Id.t -> Entries.mutual_inductive_entry -> MutInd.t
 
 (** Extra universe constraints *)
-- 
cgit v1.2.3


From 14150241cfd016c7f64974cc5c58bb116689f3c1 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Thu, 2 Jul 2020 18:17:24 +0200
Subject: [vernac] Allow to control typing flags with attributes.

The syntax is the one of boolean attributes, that is to say
`#[typing($flag={yes,no}]` where `$flag` is one of `guarded`,
`universes`, `positive`.

We had to instrument the pretyper in a few places, it is interesting
that it is doing so many checks.
---
 .../12-misc/12586-declare+typing_flags.rst         |  5 +-
 doc/sphinx/language/core/inductive.rst             | 26 ++++-----
 doc/sphinx/proof-engine/vernacular-commands.rst    | 15 +++++
 test-suite/success/typing_flags.v                  | 54 ++++++++++++++++++
 vernac/attributes.ml                               | 43 ++++++++++++++
 vernac/attributes.mli                              |  3 +
 vernac/comDefinition.ml                            | 10 ++--
 vernac/comDefinition.mli                           |  2 +
 vernac/comFixpoint.ml                              | 33 +++++------
 vernac/comFixpoint.mli                             | 23 ++++++--
 vernac/comInductive.ml                             |  8 ++-
 vernac/comInductive.mli                            |  1 +
 vernac/comProgramFixpoint.ml                       | 27 +++++----
 vernac/comProgramFixpoint.mli                      |  1 +
 vernac/declare.ml                                  |  7 ++-
 vernac/declareInd.ml                               |  8 +--
 vernac/declareInd.mli                              |  1 +
 vernac/vernacentries.ml                            | 65 ++++++++++++++--------
 18 files changed, 245 insertions(+), 87 deletions(-)

diff --git a/doc/changelog/12-misc/12586-declare+typing_flags.rst b/doc/changelog/12-misc/12586-declare+typing_flags.rst
index 001cd600b0..bd4e6f401d 100644
--- a/doc/changelog/12-misc/12586-declare+typing_flags.rst
+++ b/doc/changelog/12-misc/12586-declare+typing_flags.rst
@@ -1,5 +1,6 @@
 - **Added:**
-  Typing flags can now be specified per-constant, this does allow
-  to fine-grain specify them from plugins or attributes.
+  Typing flags can now be specified per-constant / inductive, this
+  allows to fine-grain specify them from plugins or attributes. See
+  the reference manual for details on attribute syntax.
   (`#12586 <https://github.com/coq/coq/pull/12586>`_,
   by Emilio Jesus Gallego Arias).
diff --git a/doc/sphinx/language/core/inductive.rst b/doc/sphinx/language/core/inductive.rst
index 9fda2ab1fa..f277997094 100644
--- a/doc/sphinx/language/core/inductive.rst
+++ b/doc/sphinx/language/core/inductive.rst
@@ -31,8 +31,8 @@ Inductive types
    proposition).
 
    This command supports the :attr:`universes(polymorphic)`,
-   :attr:`universes(template)`, :attr:`universes(cumulative)`, and
-   :attr:`private(matching)` attributes.
+   :attr:`universes(template)`, :attr:`universes(cumulative)`,
+   :attr:`typing(positive)`, and :attr:`private(matching)` attributes.
 
    Mutually inductive types can be defined by including multiple :n:`@inductive_definition`\s.
    The :n:`@ident`\s are simultaneously added to the environment before the types of constructors are checked.
@@ -49,10 +49,12 @@ Inductive types
 
    .. exn:: Non strictly positive occurrence of @ident in @type.
 
-      The types of the constructors have to satisfy a *positivity condition*
-      (see Section :ref:`positivity`). This condition ensures the soundness of
-      the inductive definition. The positivity checking can be disabled using
-      the :flag:`Positivity Checking` flag (see :ref:`controlling-typing-flags`).
+      The types of the constructors have to satisfy a *positivity
+      condition* (see Section :ref:`positivity`). This condition
+      ensures the soundness of the inductive definition. The
+      positivity checking can be disabled using the :flag:`Positivity
+      Checking` flag or the :attr:`typing(positive)` attribute (see
+      :ref:`controlling-typing-flags`).
 
    .. exn:: The conclusion of @type is not valid; it must be built from @ident.
 
@@ -848,9 +850,7 @@ between universes for inductive types in the Type hierarchy.
 
    .. coqtop:: none
 
-      Unset Positivity Checking.
-      Inductive I : Prop := not_I_I (not_I : I -> False) : I.
-      Set Positivity Checking.
+      #[typing(positive=no)] Inductive I : Prop := not_I_I (not_I : I -> False) : I.
 
    .. coqtop:: all
 
@@ -884,9 +884,7 @@ between universes for inductive types in the Type hierarchy.
 
    .. coqtop:: none
 
-      Unset Positivity Checking.
-      Inductive Lam := lam (_ : Lam -> Lam).
-      Set Positivity Checking.
+      #[typing(positive=no)] Inductive Lam := lam (_ : Lam -> Lam).
 
    .. coqtop:: all
 
@@ -915,9 +913,7 @@ between universes for inductive types in the Type hierarchy.
 
    .. coqtop:: none
 
-      Unset Positivity Checking.
-      Inductive A: Type := introA: ((A -> Prop) -> Prop) -> A.
-      Set Positivity Checking.
+      #[typing(positive=no)] Inductive A: Type := introA: ((A -> Prop) -> Prop) -> A.
 
    .. coqtop:: all
 
diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst
index e7db9cfaca..b8160b7966 100644
--- a/doc/sphinx/proof-engine/vernacular-commands.rst
+++ b/doc/sphinx/proof-engine/vernacular-commands.rst
@@ -1152,6 +1152,11 @@ Controlling Typing Flags
    anymore but it still affects the reduction of the term. Unchecked fixpoints are
    printed by :cmd:`Print Assumptions`.
 
+.. attr:: typing(guarded)
+
+   Similar to :flag:`Guard Checking`, but on a per-declaration
+   basis. Takes ``yes/no`` as parameters, i.e. ``typing(guarded=no)``.
+
 .. flag:: Positivity Checking
 
    This flag can be used to enable/disable the positivity checking of inductive
@@ -1159,6 +1164,11 @@ Controlling Typing Flags
    break the consistency of the system, use at your own risk. Unchecked
    (co)inductive types are printed by :cmd:`Print Assumptions`.
 
+.. attr:: typing(positive)
+
+   Similar to :flag:`Positivity Checking`, but on a per-declaration basis.
+   Takes ``yes/no`` as parameters, i.e. ``typing(positive=no)``.
+
 .. flag:: Universe Checking
 
    This flag can be used to enable/disable the checking of universes, providing a
@@ -1167,6 +1177,11 @@ Controlling Typing Flags
    :cmd:`Print Assumptions`. It has the same effect as `-type-in-type` command line
    argument (see :ref:`command-line-options`).
 
+.. attr:: typing(universes)
+
+   Similar to :flag:`Universe Checking`, but on a per-declaration basis.
+   Takes ``yes/no`` as parameters, i.e. ``typing(universes=no)``.
+
 .. cmd:: Print Typing Flags
 
    Print the status of the three typing flags: guard checking, positivity checking
diff --git a/test-suite/success/typing_flags.v b/test-suite/success/typing_flags.v
index bd20d9c804..a6640a5a03 100644
--- a/test-suite/success/typing_flags.v
+++ b/test-suite/success/typing_flags.v
@@ -1,4 +1,58 @@
+From Coq Require Import Program.Tactics.
 
+(* Part using attributes *)
+
+#[typing(guarded=no)] Fixpoint att_f' (n : nat) : nat := att_f' n.
+#[typing(guarded=no)] Program Fixpoint p_att_f' (n : nat) : nat := p_att_f' n.
+
+#[typing(universes=no)] Definition att_T := let t := Type in (t : t).
+#[typing(universes=no)] Program Definition p_att_T := let t := Type in (t : t).
+
+#[typing(positive=no)]
+Inductive att_Cor :=
+| att_Over : att_Cor
+| att_Next : ((att_Cor -> list nat) -> list nat) -> att_Cor.
+
+Fail #[typing(guarded=yes)] Fixpoint f_att_f' (n : nat) : nat := f_att_f' n.
+Fail #[typing(universes=yes)] Definition f_att_T := let t := Type in (t : t).
+
+Fail #[typing(positive=yes)]
+Inductive f_att_Cor :=
+| f_att_Over : f_att_Cor
+| f_att_Next : ((f_att_Cor -> list nat) -> list nat) -> f_att_Cor.
+
+Print Assumptions att_f'.
+Print Assumptions att_T.
+Print Assumptions att_Cor.
+
+(* Interactive + atts *)
+
+(* Coq's handling of environments in tactic mode is too broken for this to work yet *)
+
+(*
+#[typing(universes=no)] Definition i_att_T' : Type. Proof. exact (let t := Type in (t : t)). Defined.
+#[typing(universes=no)] Definition d_att_T' : Type. Proof. exact (let t := Type in (t : t)). Qed.
+#[typing(universes=no)] Program Definition pi_att_T' : Type. Proof. exact (let t := Type in (t : t)). Qed.
+*)
+
+(* Note: this works a bit by chance, the attribute only affects the
+   kernel call in Defined. Would the tactics perform a check we would
+   fail. *)
+#[typing(guarded=no)] Fixpoint i_att_f' (n : nat) : nat.
+Proof. exact (i_att_f' n). Defined.
+
+#[typing(guarded=no)] Fixpoint d_att_f' (n : nat) : nat.
+Proof. exact (d_att_f' n). Qed.
+
+(* check regular mode is still safe *)
+Fail Fixpoint f_att_f' (n : nat) : nat := f_att_f' n.
+Fail Definition f_att_T := let t := Type in (t : t).
+
+Fail Inductive f_att_Cor :=
+| f_att_Over : f_att_Cor
+| f_att_Next : ((f_att_Cor -> list nat) -> list nat) -> f_att_Cor.
+
+(* Part using Set/Unset *)
 Print Typing Flags.
 Unset Guard Checking.
 Fixpoint f' (n : nat) : nat := f' n.
diff --git a/vernac/attributes.ml b/vernac/attributes.ml
index fdaeedef8c..05d96a1165 100644
--- a/vernac/attributes.ml
+++ b/vernac/attributes.ml
@@ -338,3 +338,46 @@ 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 enable =
+  match att with
+  | "universes" ->
+    { typing_flags with
+      Declarations.check_universes = enable
+    }
+  | "guarded" ->
+    { typing_flags with
+      Declarations.check_guarded = enable
+    }
+  | "positive" ->
+    { typing_flags with
+      Declarations.check_positive = enable
+    }
+  | att ->
+    CErrors.user_err Pp.(str "Unknown “typing” attribute: " ++ str att)
+
+let process_typing_enable ~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 enable = process_typing_enable ~key:typing_att enable in
+      let typing_flags = process_typing_att ~typing_flags typing_att enable 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 ["typing", 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..3f2f0f8755 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 = Option.cata (fun typing_flags -> Environ.set_typing_flags typing_flags env) env typing_flags 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 = Option.cata (fun typing_flags -> Environ.set_typing_flags typing_flags env) env typing_flags 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..1184cd96ac 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 = Option.cata (fun typing_flags -> Environ.set_typing_flags typing_flags env) env typing_flags 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..5c859e2f01 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 = Option.cata (fun typing_flags -> Environ.set_typing_flags typing_flags env) env typing_flags 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..9033df1673 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 = Option.cata (fun typing_flags -> Environ.set_typing_flags typing_flags env) env typing_flags 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 = Option.cata (fun typing_flags -> Environ.set_typing_flags typing_flags env) env typing_flags in
+        Pretyping.search_guard env possible_indexes fixdecls in
+      let env = Option.cata (fun typing_flags -> Environ.set_typing_flags typing_flags env) env typing_flags 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 210007d17d..4921ce0f0d 100644
--- a/vernac/declare.ml
+++ b/vernac/declare.ml
@@ -584,10 +584,11 @@ let declare_entry_core ~name ~scope ~kind ~typing_flags ?hook ~obls ~impargs ~uc
 
 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 = Option.cata (fun typing_flags -> Environ.set_typing_flags typing_flags env) env typing_flags 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
@@ -600,7 +601,7 @@ let mutual_make_bodies ~fixitems ~rec_declaration ~possible_indexes =
 let declare_mutually_recursive_core ~info ~cinfo ~opaque ~ntns ~uctx ~rec_declaration ~possible_indexes ?(restrict_ucontext=true) () =
   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
@@ -1915,6 +1916,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 = Option.cata (fun typing_flags -> Environ.set_typing_flags typing_flags env) env typing_flags in
       Internal.map_entry_body entry
         ~f:(guess_decreasing env possible_indexes)
     in
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..0801d8d83f 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 = Option.cata (fun typing_flags -> Environ.set_typing_flags typing_flags env0) env0 typing_flags 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 =
-- 
cgit v1.2.3


From 454a10da9412a5bd6f3661b1f60e17f08289d0e5 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Fri, 16 Oct 2020 17:13:14 +0200
Subject: [proofs] Support per-definition typing-flags in interactive proofs.

Most cases should be accounted in proof code, however be wary of paths
where `Global.env ()` is used.
---
 proofs/proof.ml                   | 8 ++++++--
 proofs/proof.mli                  | 2 ++
 test-suite/success/typing_flags.v | 5 ++---
 vernac/declare.ml                 | 7 ++++---
 4 files changed, 14 insertions(+), 8 deletions(-)

diff --git a/proofs/proof.ml b/proofs/proof.ml
index 24f3ac3f29..e9c8ce6746 100644
--- a/proofs/proof.ml
+++ b/proofs/proof.ml
@@ -115,6 +115,7 @@ type t =
   (** the name of the theorem whose proof is being constructed *)
   ; poly : bool
   (** polymorphism *)
+  ; typing_flags : Declarations.typing_flags option
   }
 
 (*** General proof functions ***)
@@ -278,7 +279,7 @@ let end_of_stack = CondEndStack end_of_stack_kind
 
 let unfocused = is_last_focus end_of_stack_kind
 
-let start ~name ~poly sigma goals =
+let start ~name ~poly ?typing_flags sigma goals =
   let entry, proofview = Proofview.init sigma goals in
   let pr =
     { proofview
@@ -286,10 +287,11 @@ let start ~name ~poly sigma goals =
     ; focus_stack = []
     ; name
     ; poly
+    ; typing_flags
   } in
   _focus end_of_stack (Obj.repr ()) 1 (List.length goals) pr
 
-let dependent_start ~name ~poly goals =
+let dependent_start ~name ~poly ?typing_flags goals =
   let entry, proofview = Proofview.dependent_init goals in
   let pr =
     { proofview
@@ -297,6 +299,7 @@ let dependent_start ~name ~poly goals =
     ; focus_stack = []
     ; name
     ; poly
+    ; typing_flags
   } in
   let number_of_goals = List.length (Proofview.initial_goals pr.entry) in
   _focus end_of_stack (Obj.repr ()) 1 number_of_goals pr
@@ -560,6 +563,7 @@ let solve ?with_end_tac gi info_lvl tac pr =
       else tac
     in
     let env = Global.env () in
+    let env = Option.cata (fun f -> Environ.set_typing_flags f env) env pr.typing_flags in
     let (p,(status,info),()) = run_tactic env tac pr in
     let env = Global.env () in
     let sigma = Evd.from_env env in
diff --git a/proofs/proof.mli b/proofs/proof.mli
index f487595dac..a527820c7a 100644
--- a/proofs/proof.mli
+++ b/proofs/proof.mli
@@ -55,11 +55,13 @@ val data : t -> data
 val start
   :  name:Names.Id.t
   -> poly:bool
+  -> ?typing_flags:Declarations.typing_flags
   -> Evd.evar_map -> (Environ.env * EConstr.types) list -> t
 
 val dependent_start
   :  name:Names.Id.t
   -> poly:bool
+  -> ?typing_flags:Declarations.typing_flags
   -> Proofview.telescope -> t
 
 (* Returns [true] if the considered proof is completed, that is if no goal remain
diff --git a/test-suite/success/typing_flags.v b/test-suite/success/typing_flags.v
index a6640a5a03..a5fe676cc1 100644
--- a/test-suite/success/typing_flags.v
+++ b/test-suite/success/typing_flags.v
@@ -27,13 +27,12 @@ Print Assumptions att_Cor.
 
 (* Interactive + atts *)
 
-(* Coq's handling of environments in tactic mode is too broken for this to work yet *)
+(* Coq's handling of environments in tactic mode is too broken for
+   this to work yet, the pretyper doesn't get the right flags *)
 
-(*
 #[typing(universes=no)] Definition i_att_T' : Type. Proof. exact (let t := Type in (t : t)). Defined.
 #[typing(universes=no)] Definition d_att_T' : Type. Proof. exact (let t := Type in (t : t)). Qed.
 #[typing(universes=no)] Program Definition pi_att_T' : Type. Proof. exact (let t := Type in (t : t)). Qed.
-*)
 
 (* Note: this works a bit by chance, the attribute only affects the
    kernel call in Defined. Would the tactics perform a check we would
diff --git a/vernac/declare.ml b/vernac/declare.ml
index 4921ce0f0d..74ace04a7c 100644
--- a/vernac/declare.ml
+++ b/vernac/declare.ml
@@ -1428,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
@@ -1451,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
-- 
cgit v1.2.3


From 2ac3d11f6f1332250e918ef628eca3b788b3550a Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Fri, 16 Oct 2020 20:06:26 +0200
Subject: [environ] [typing_flags] Introduce helper function to remove
 duplicate code

---
 kernel/environ.ml            | 3 +++
 kernel/environ.mli           | 3 +++
 proofs/proof.ml              | 2 +-
 vernac/comDefinition.ml      | 4 ++--
 vernac/comFixpoint.ml        | 2 +-
 vernac/comInductive.ml       | 2 +-
 vernac/comProgramFixpoint.ml | 6 +++---
 vernac/declare.ml            | 4 ++--
 vernac/vernacentries.ml      | 2 +-
 9 files changed, 17 insertions(+), 11 deletions(-)

diff --git a/kernel/environ.ml b/kernel/environ.ml
index 69edb1498c..a5f81d1e59 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -479,6 +479,9 @@ let set_typing_flags c env =
     let env = set_type_in_type (not c.check_universes) env in
     env
 
+let update_typing_flags ?typing_flags env =
+  Option.cata (fun flags -> set_typing_flags flags env) env typing_flags
+
 let set_cumulative_sprop b env =
   set_typing_flags {env.env_typing_flags with cumulative_sprop=b} env
 
diff --git a/kernel/environ.mli b/kernel/environ.mli
index 6a8ddce835..900e2128ea 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -351,6 +351,9 @@ val set_type_in_type : bool -> env -> env
 val set_allow_sprop : bool -> env -> env
 val sprop_allowed : env -> bool
 
+(** [update_typing_flags ?typing_flags] may update env with optional typing flags *)
+val update_typing_flags : ?typing_flags:typing_flags -> env -> env
+
 val universes_of_global : env -> GlobRef.t -> AUContext.t
 
 (** {6 Sets of referred section variables }
diff --git a/proofs/proof.ml b/proofs/proof.ml
index e9c8ce6746..50a0e63700 100644
--- a/proofs/proof.ml
+++ b/proofs/proof.ml
@@ -563,7 +563,7 @@ let solve ?with_end_tac gi info_lvl tac pr =
       else tac
     in
     let env = Global.env () in
-    let env = Option.cata (fun f -> Environ.set_typing_flags f env) env pr.typing_flags in
+    let env = Environ.update_typing_flags ?typing_flags:pr.typing_flags env in
     let (p,(status,info),()) = run_tactic env tac pr in
     let env = Global.env () in
     let sigma = Evd.from_env env in
diff --git a/vernac/comDefinition.ml b/vernac/comDefinition.ml
index 3f2f0f8755..c54adb45f9 100644
--- a/vernac/comDefinition.ml
+++ b/vernac/comDefinition.ml
@@ -113,7 +113,7 @@ let interp_definition ~program_mode env evd impl_env 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 = Option.cata (fun typing_flags -> Environ.set_typing_flags typing_flags env) env typing_flags 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 =
@@ -134,7 +134,7 @@ let do_definition ?hook ~name ~scope ~poly ?typing_flags ~kind ?using udecl bl r
 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 = Option.cata (fun typing_flags -> Environ.set_typing_flags typing_flags env) env typing_flags 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 =
diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml
index 1184cd96ac..0cf0b07822 100644
--- a/vernac/comFixpoint.ml
+++ b/vernac/comFixpoint.ml
@@ -245,7 +245,7 @@ let interp_fixpoint ?(check_recursivity=true) ?typing_flags ~cofix l :
     UState.universe_decl * UState.t *
     (EConstr.rel_context * Impargs.manual_implicits * int option) list) =
   let env = Global.env () in
-  let env = Option.cata (fun typing_flags -> Environ.set_typing_flags typing_flags env) env typing_flags 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
diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml
index 5c859e2f01..2be6097184 100644
--- a/vernac/comInductive.ml
+++ b/vernac/comInductive.ml
@@ -641,7 +641,7 @@ let do_mutual_inductive ~template udecl indl ~cumulative ~poly ?typing_flags ~pr
       | NonUniformParameters -> ([], params, indl)
   in
   let env = Global.env () in
-  let env = Option.cata (fun typing_flags -> Environ.set_typing_flags typing_flags env) env typing_flags 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 ?typing_flags mie pl impls);
diff --git a/vernac/comProgramFixpoint.ml b/vernac/comProgramFixpoint.ml
index 9033df1673..3c4a651cf5 100644
--- a/vernac/comProgramFixpoint.ml
+++ b/vernac/comProgramFixpoint.ml
@@ -284,7 +284,7 @@ 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 =
     let env = Global.env () in
-    let env = Option.cata (fun typing_flags -> Environ.set_typing_flags typing_flags env) env typing_flags in
+    let env = Environ.update_typing_flags ?typing_flags env in
     interp_recursive env ~cofix ~program_mode:true fixl
   in
     (* Program-specific code *)
@@ -323,9 +323,9 @@ let do_program_recursive ~pm ~scope ~poly ?typing_flags ?using fixkind fixl =
       in
       let indexes =
         let env = Global.env () in
-        let env = Option.cata (fun typing_flags -> Environ.set_typing_flags typing_flags env) env typing_flags in
+        let env = Environ.update_typing_flags ?typing_flags env in
         Pretyping.search_guard env possible_indexes fixdecls in
-      let env = Option.cata (fun typing_flags -> Environ.set_typing_flags typing_flags env) env typing_flags in
+      let env = Environ.update_typing_flags ?typing_flags env in
       List.iteri (fun i _ ->
           Inductive.check_fix env
             ((indexes,i),fixdecls))
diff --git a/vernac/declare.ml b/vernac/declare.ml
index 74ace04a7c..fafee13bf6 100644
--- a/vernac/declare.ml
+++ b/vernac/declare.ml
@@ -588,7 +588,7 @@ let mutual_make_bodies ~typing_flags ~fixitems ~rec_declaration ~possible_indexe
   match possible_indexes with
   | Some possible_indexes ->
     let env = Global.env() in
-    let env = Option.cata (fun typing_flags -> Environ.set_typing_flags typing_flags env) env typing_flags 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
@@ -1918,7 +1918,7 @@ end = struct
       (* Try all combinations... not optimal *)
       let env = Global.env() in
       let typing_flags = pinfo.Proof_info.info.Info.typing_flags in
-      let env = Option.cata (fun typing_flags -> Environ.set_typing_flags typing_flags env) env 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
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 0801d8d83f..a3726daf63 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -550,7 +550,7 @@ let post_check_evd ~udecl ~poly evd =
 
 let start_lemma_com ~typing_flags ~program_mode ~poly ~scope ~kind ?using ?hook thms =
   let env0 = Global.env () in
-  let env0 = Option.cata (fun typing_flags -> Environ.set_typing_flags typing_flags env0) env0 typing_flags 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
-- 
cgit v1.2.3


From 50af46a596af607493ce46da782389e8a82e8354 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Wed, 18 Nov 2020 23:25:17 +0100
Subject: [attributes] [doc] Documentation review by Théo.

Co-authored-by: <Théo Zimmermann <theo.zimmermann@inria.fr>
---
 doc/changelog/12-misc/12586-declare+typing_flags.rst |  2 +-
 doc/sphinx/language/core/coinductive.rst             |  3 ++-
 doc/sphinx/language/core/definitions.rst             |  8 +++++---
 doc/sphinx/language/core/inductive.rst               | 10 ++++++----
 doc/sphinx/proof-engine/vernacular-commands.rst      | 15 +++++++++------
 test-suite/success/typing_flags.v                    |  8 +-------
 6 files changed, 24 insertions(+), 22 deletions(-)

diff --git a/doc/changelog/12-misc/12586-declare+typing_flags.rst b/doc/changelog/12-misc/12586-declare+typing_flags.rst
index bd4e6f401d..52915ceee9 100644
--- a/doc/changelog/12-misc/12586-declare+typing_flags.rst
+++ b/doc/changelog/12-misc/12586-declare+typing_flags.rst
@@ -1,6 +1,6 @@
 - **Added:**
   Typing flags can now be specified per-constant / inductive, this
   allows to fine-grain specify them from plugins or attributes. See
-  the reference manual for details on attribute syntax.
+  :ref:`controlling-typing-flags` for details on attribute syntax.
   (`#12586 <https://github.com/coq/coq/pull/12586>`_,
   by Emilio Jesus Gallego Arias).
diff --git a/doc/sphinx/language/core/coinductive.rst b/doc/sphinx/language/core/coinductive.rst
index 43bbc8b40d..e9737f8712 100644
--- a/doc/sphinx/language/core/coinductive.rst
+++ b/doc/sphinx/language/core/coinductive.rst
@@ -27,7 +27,8 @@ More information on co-inductive definitions can be found in
 
    This command supports the :attr:`universes(polymorphic)`,
    :attr:`universes(template)`, :attr:`universes(cumulative)`,
-   :attr:`private(matching)`, and :attr:`using` attributes.
+   :attr:`private(matching)`, :attr:`typing(universes)`,
+   :attr:`typing(positive)`, and :attr:`using` attributes.
 
 .. example::
 
diff --git a/doc/sphinx/language/core/definitions.rst b/doc/sphinx/language/core/definitions.rst
index 57771c9036..95bb1b0e0c 100644
--- a/doc/sphinx/language/core/definitions.rst
+++ b/doc/sphinx/language/core/definitions.rst
@@ -90,8 +90,9 @@ Section :ref:`typing-rules`.
    computation on :n:`@term`.
 
    These commands also support the :attr:`universes(polymorphic)`,
-   :attr:`program` (see :ref:`program_definition`),
-   :attr:`canonical` and :attr:`using` attributes.
+   :attr:`program` (see :ref:`program_definition`), :attr:`canonical`,
+   :attr:`typing(universes)`, :attr:`typing(guarded)`, and
+   :attr:`using` attributes.
 
    If :n:`@term` is omitted, :n:`@type` is required and Coq enters proof editing mode.
    This can be used to define a term incrementally, in particular by relying on the :tacn:`refine` tactic.
@@ -162,7 +163,8 @@ Chapter :ref:`Tactics`. The basic assertion command is:
    correct at some time of the interactive development of a proof, use the
    command :cmd:`Guarded`.
 
-   This command accepts the :attr:`using` attribute.
+   This command accepts the :attr:`typing(universes)`,
+   :attr:`typing(guarded)`, and :attr:`using` attributes.
 
    .. exn:: The term @term has type @type which should be Set, Prop or Type.
       :undocumented:
diff --git a/doc/sphinx/language/core/inductive.rst b/doc/sphinx/language/core/inductive.rst
index f277997094..86de059f28 100644
--- a/doc/sphinx/language/core/inductive.rst
+++ b/doc/sphinx/language/core/inductive.rst
@@ -32,7 +32,8 @@ Inductive types
 
    This command supports the :attr:`universes(polymorphic)`,
    :attr:`universes(template)`, :attr:`universes(cumulative)`,
-   :attr:`typing(positive)`, and :attr:`private(matching)` attributes.
+   :attr:`typing(positive)`, :attr:`typing(universes)`, and
+   :attr:`private(matching)` attributes.
 
    Mutually inductive types can be defined by including multiple :n:`@inductive_definition`\s.
    The :n:`@ident`\s are simultaneously added to the environment before the types of constructors are checked.
@@ -51,8 +52,8 @@ Inductive types
 
       The types of the constructors have to satisfy a *positivity
       condition* (see Section :ref:`positivity`). This condition
-      ensures the soundness of the inductive definition. The
-      positivity checking can be disabled using the :flag:`Positivity
+      ensures the soundness of the inductive definition.
+      Positivity checking can be disabled using the :flag:`Positivity
       Checking` flag or the :attr:`typing(positive)` attribute (see
       :ref:`controlling-typing-flags`).
 
@@ -392,7 +393,8 @@ constructions.
    consequently :n:`forall {* @binder }, @type` and its value is equivalent
    to :n:`fun {* @binder } => @term`.
 
-   This command accepts the :attr:`program` attribute.
+   This command accepts the :attr:`program`,
+   :attr:`typing(universes)`, and :attr:`typing(guarded)` attributes.
 
    To be accepted, a :cmd:`Fixpoint` definition has to satisfy syntactical
    constraints on a special argument called the decreasing argument. They
diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst
index b8160b7966..08534c9e07 100644
--- a/doc/sphinx/proof-engine/vernacular-commands.rst
+++ b/doc/sphinx/proof-engine/vernacular-commands.rst
@@ -1152,10 +1152,11 @@ Controlling Typing Flags
    anymore but it still affects the reduction of the term. Unchecked fixpoints are
    printed by :cmd:`Print Assumptions`.
 
-.. attr:: typing(guarded)
+.. attr:: typing(guarded{? = {| yes | no } })
+   :name: typing(guarded)
 
    Similar to :flag:`Guard Checking`, but on a per-declaration
-   basis. Takes ``yes/no`` as parameters, i.e. ``typing(guarded=no)``.
+   basis. Disable guard checking locally with ``typing(guarded=no)``.
 
 .. flag:: Positivity Checking
 
@@ -1164,10 +1165,11 @@ Controlling Typing Flags
    break the consistency of the system, use at your own risk. Unchecked
    (co)inductive types are printed by :cmd:`Print Assumptions`.
 
-.. attr:: typing(positive)
+.. attr:: typing(positive{? = {| yes | no } })
+   :name: typing(positive)
 
    Similar to :flag:`Positivity Checking`, but on a per-declaration basis.
-   Takes ``yes/no`` as parameters, i.e. ``typing(positive=no)``.
+   Disable positivity checking locally with ``typing(positive=no)``.
 
 .. flag:: Universe Checking
 
@@ -1177,10 +1179,11 @@ Controlling Typing Flags
    :cmd:`Print Assumptions`. It has the same effect as `-type-in-type` command line
    argument (see :ref:`command-line-options`).
 
-.. attr:: typing(universes)
+.. attr:: typing(universes{? = {| yes | no } })
+   :name: typing(universes)
 
    Similar to :flag:`Universe Checking`, but on a per-declaration basis.
-   Takes ``yes/no`` as parameters, i.e. ``typing(universes=no)``.
+   Disable universe checking locally with ``typing(universe=no)``.
 
 .. cmd:: Print Typing Flags
 
diff --git a/test-suite/success/typing_flags.v b/test-suite/success/typing_flags.v
index a5fe676cc1..4a20f3379b 100644
--- a/test-suite/success/typing_flags.v
+++ b/test-suite/success/typing_flags.v
@@ -26,17 +26,11 @@ Print Assumptions att_T.
 Print Assumptions att_Cor.
 
 (* Interactive + atts *)
-
-(* Coq's handling of environments in tactic mode is too broken for
-   this to work yet, the pretyper doesn't get the right flags *)
-
 #[typing(universes=no)] Definition i_att_T' : Type. Proof. exact (let t := Type in (t : t)). Defined.
 #[typing(universes=no)] Definition d_att_T' : Type. Proof. exact (let t := Type in (t : t)). Qed.
 #[typing(universes=no)] Program Definition pi_att_T' : Type. Proof. exact (let t := Type in (t : t)). Qed.
 
-(* Note: this works a bit by chance, the attribute only affects the
-   kernel call in Defined. Would the tactics perform a check we would
-   fail. *)
+(* Note: be aware of tactics invoking [Global.env()] if this test fails. *)
 #[typing(guarded=no)] Fixpoint i_att_f' (n : nat) : nat.
 Proof. exact (i_att_f' n). Defined.
 
-- 
cgit v1.2.3


From 1f0f1ae93f757be8101d598f8aaf5b564bde9dcd Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Thu, 26 Nov 2020 21:32:37 +0100
Subject: [attributes] [typing] Rename `typing` to `bypass_check`

As discussed in the Coq meeting.
---
 doc/sphinx/language/core/coinductive.rst        |  4 ++--
 doc/sphinx/language/core/definitions.rst        |  6 +++---
 doc/sphinx/language/core/inductive.rst          | 12 ++++++------
 doc/sphinx/proof-engine/vernacular-commands.rst | 18 ++++++++---------
 test-suite/success/typing_flags.v               | 26 ++++++++++++-------------
 vernac/attributes.ml                            | 15 +++++++-------
 6 files changed, 41 insertions(+), 40 deletions(-)

diff --git a/doc/sphinx/language/core/coinductive.rst b/doc/sphinx/language/core/coinductive.rst
index e9737f8712..cf46580bdb 100644
--- a/doc/sphinx/language/core/coinductive.rst
+++ b/doc/sphinx/language/core/coinductive.rst
@@ -27,8 +27,8 @@ More information on co-inductive definitions can be found in
 
    This command supports the :attr:`universes(polymorphic)`,
    :attr:`universes(template)`, :attr:`universes(cumulative)`,
-   :attr:`private(matching)`, :attr:`typing(universes)`,
-   :attr:`typing(positive)`, and :attr:`using` attributes.
+   :attr:`private(matching)`, :attr:`bypass_check(universes)`,
+   :attr:`bypass_check(positivity)`, and :attr:`using` attributes.
 
 .. example::
 
diff --git a/doc/sphinx/language/core/definitions.rst b/doc/sphinx/language/core/definitions.rst
index 95bb1b0e0c..76aa543b8b 100644
--- a/doc/sphinx/language/core/definitions.rst
+++ b/doc/sphinx/language/core/definitions.rst
@@ -91,7 +91,7 @@ Section :ref:`typing-rules`.
 
    These commands also support the :attr:`universes(polymorphic)`,
    :attr:`program` (see :ref:`program_definition`), :attr:`canonical`,
-   :attr:`typing(universes)`, :attr:`typing(guarded)`, and
+   :attr:`bypass_check(universes)`, :attr:`bypass_check(guard)`, and
    :attr:`using` attributes.
 
    If :n:`@term` is omitted, :n:`@type` is required and Coq enters proof editing mode.
@@ -163,8 +163,8 @@ Chapter :ref:`Tactics`. The basic assertion command is:
    correct at some time of the interactive development of a proof, use the
    command :cmd:`Guarded`.
 
-   This command accepts the :attr:`typing(universes)`,
-   :attr:`typing(guarded)`, and :attr:`using` attributes.
+   This command accepts the :attr:`bypass_check(universes)`,
+   :attr:`bypass_check(guard)`, and :attr:`using` attributes.
 
    .. exn:: The term @term has type @type which should be Set, Prop or Type.
       :undocumented:
diff --git a/doc/sphinx/language/core/inductive.rst b/doc/sphinx/language/core/inductive.rst
index 86de059f28..4bee7cc1b1 100644
--- a/doc/sphinx/language/core/inductive.rst
+++ b/doc/sphinx/language/core/inductive.rst
@@ -32,7 +32,7 @@ Inductive types
 
    This command supports the :attr:`universes(polymorphic)`,
    :attr:`universes(template)`, :attr:`universes(cumulative)`,
-   :attr:`typing(positive)`, :attr:`typing(universes)`, and
+   :attr:`bypass_check(positivity)`, :attr:`bypass_check(universes)`, and
    :attr:`private(matching)` attributes.
 
    Mutually inductive types can be defined by including multiple :n:`@inductive_definition`\s.
@@ -54,7 +54,7 @@ Inductive types
       condition* (see Section :ref:`positivity`). This condition
       ensures the soundness of the inductive definition.
       Positivity checking can be disabled using the :flag:`Positivity
-      Checking` flag or the :attr:`typing(positive)` attribute (see
+      Checking` flag or the :attr:`bypass_check(positivity)` attribute (see
       :ref:`controlling-typing-flags`).
 
    .. exn:: The conclusion of @type is not valid; it must be built from @ident.
@@ -394,7 +394,7 @@ constructions.
    to :n:`fun {* @binder } => @term`.
 
    This command accepts the :attr:`program`,
-   :attr:`typing(universes)`, and :attr:`typing(guarded)` attributes.
+   :attr:`bypass_check(universes)`, and :attr:`bypass_check(guard)` attributes.
 
    To be accepted, a :cmd:`Fixpoint` definition has to satisfy syntactical
    constraints on a special argument called the decreasing argument. They
@@ -852,7 +852,7 @@ between universes for inductive types in the Type hierarchy.
 
    .. coqtop:: none
 
-      #[typing(positive=no)] Inductive I : Prop := not_I_I (not_I : I -> False) : I.
+      #[bypass_check(positivity)] Inductive I : Prop := not_I_I (not_I : I -> False) : I.
 
    .. coqtop:: all
 
@@ -886,7 +886,7 @@ between universes for inductive types in the Type hierarchy.
 
    .. coqtop:: none
 
-      #[typing(positive=no)] Inductive Lam := lam (_ : Lam -> Lam).
+      #[bypass_check(positivity)] Inductive Lam := lam (_ : Lam -> Lam).
 
    .. coqtop:: all
 
@@ -915,7 +915,7 @@ between universes for inductive types in the Type hierarchy.
 
    .. coqtop:: none
 
-      #[typing(positive=no)] Inductive A: Type := introA: ((A -> Prop) -> Prop) -> A.
+      #[bypass_check(positivity)] Inductive A: Type := introA: ((A -> Prop) -> Prop) -> A.
 
    .. coqtop:: all
 
diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst
index 08534c9e07..e866e4c624 100644
--- a/doc/sphinx/proof-engine/vernacular-commands.rst
+++ b/doc/sphinx/proof-engine/vernacular-commands.rst
@@ -1152,11 +1152,11 @@ Controlling Typing Flags
    anymore but it still affects the reduction of the term. Unchecked fixpoints are
    printed by :cmd:`Print Assumptions`.
 
-.. attr:: typing(guarded{? = {| yes | no } })
-   :name: typing(guarded)
+.. attr:: bypass_check(guard{? = {| yes | no } })
+   :name: bypass_check(guard)
 
    Similar to :flag:`Guard Checking`, but on a per-declaration
-   basis. Disable guard checking locally with ``typing(guarded=no)``.
+   basis. Disable guard checking locally with ``bypass_check(guard)``.
 
 .. flag:: Positivity Checking
 
@@ -1165,11 +1165,11 @@ Controlling Typing Flags
    break the consistency of the system, use at your own risk. Unchecked
    (co)inductive types are printed by :cmd:`Print Assumptions`.
 
-.. attr:: typing(positive{? = {| yes | no } })
-   :name: typing(positive)
+.. attr:: bypass_check(positivity{? = {| yes | no } })
+   :name: bypass_check(positivity)
 
    Similar to :flag:`Positivity Checking`, but on a per-declaration basis.
-   Disable positivity checking locally with ``typing(positive=no)``.
+   Disable positivity checking locally with ``bypass_check(positivity)``.
 
 .. flag:: Universe Checking
 
@@ -1179,11 +1179,11 @@ Controlling Typing Flags
    :cmd:`Print Assumptions`. It has the same effect as `-type-in-type` command line
    argument (see :ref:`command-line-options`).
 
-.. attr:: typing(universes{? = {| yes | no } })
-   :name: typing(universes)
+.. attr:: bypass_check(universes{? = {| yes | no } })
+   :name: bypass_check(universes)
 
    Similar to :flag:`Universe Checking`, but on a per-declaration basis.
-   Disable universe checking locally with ``typing(universe=no)``.
+   Disable universe checking locally with ``bypass_check(universes)``.
 
 .. cmd:: Print Typing Flags
 
diff --git a/test-suite/success/typing_flags.v b/test-suite/success/typing_flags.v
index 4a20f3379b..4af2028e38 100644
--- a/test-suite/success/typing_flags.v
+++ b/test-suite/success/typing_flags.v
@@ -2,21 +2,21 @@ From Coq Require Import Program.Tactics.
 
 (* Part using attributes *)
 
-#[typing(guarded=no)] Fixpoint att_f' (n : nat) : nat := att_f' n.
-#[typing(guarded=no)] Program Fixpoint p_att_f' (n : nat) : nat := p_att_f' n.
+#[bypass_check(guard)] Fixpoint att_f' (n : nat) : nat := att_f' n.
+#[bypass_check(guard)] Program Fixpoint p_att_f' (n : nat) : nat := p_att_f' n.
 
-#[typing(universes=no)] Definition att_T := let t := Type in (t : t).
-#[typing(universes=no)] Program Definition p_att_T := let t := Type in (t : t).
+#[bypass_check(universes)] Definition att_T := let t := Type in (t : t).
+#[bypass_check(universes)] Program Definition p_att_T := let t := Type in (t : t).
 
-#[typing(positive=no)]
+#[bypass_check(positivity)]
 Inductive att_Cor :=
 | att_Over : att_Cor
 | att_Next : ((att_Cor -> list nat) -> list nat) -> att_Cor.
 
-Fail #[typing(guarded=yes)] Fixpoint f_att_f' (n : nat) : nat := f_att_f' n.
-Fail #[typing(universes=yes)] Definition f_att_T := let t := Type in (t : t).
+Fail #[bypass_check(guard=no)] Fixpoint f_att_f' (n : nat) : nat := f_att_f' n.
+Fail #[bypass_check(universes=no)] Definition f_att_T := let t := Type in (t : t).
 
-Fail #[typing(positive=yes)]
+Fail #[bypass_check(positivity=no)]
 Inductive f_att_Cor :=
 | f_att_Over : f_att_Cor
 | f_att_Next : ((f_att_Cor -> list nat) -> list nat) -> f_att_Cor.
@@ -26,15 +26,15 @@ Print Assumptions att_T.
 Print Assumptions att_Cor.
 
 (* Interactive + atts *)
-#[typing(universes=no)] Definition i_att_T' : Type. Proof. exact (let t := Type in (t : t)). Defined.
-#[typing(universes=no)] Definition d_att_T' : Type. Proof. exact (let t := Type in (t : t)). Qed.
-#[typing(universes=no)] Program Definition pi_att_T' : Type. Proof. exact (let t := Type in (t : t)). Qed.
+#[bypass_check(universes=yes)] Definition i_att_T' : Type. Proof. exact (let t := Type in (t : t)). Defined.
+#[bypass_check(universes=yes)] Definition d_att_T' : Type. Proof. exact (let t := Type in (t : t)). Qed.
+#[bypass_check(universes=yes)] Program Definition pi_att_T' : Type. Proof. exact (let t := Type in (t : t)). Qed.
 
 (* Note: be aware of tactics invoking [Global.env()] if this test fails. *)
-#[typing(guarded=no)] Fixpoint i_att_f' (n : nat) : nat.
+#[bypass_check(guard=yes)] Fixpoint i_att_f' (n : nat) : nat.
 Proof. exact (i_att_f' n). Defined.
 
-#[typing(guarded=no)] Fixpoint d_att_f' (n : nat) : nat.
+#[bypass_check(guard=yes)] Fixpoint d_att_f' (n : nat) : nat.
 Proof. exact (d_att_f' n). Qed.
 
 (* check regular mode is still safe *)
diff --git a/vernac/attributes.ml b/vernac/attributes.ml
index 05d96a1165..37895d22f5 100644
--- a/vernac/attributes.ml
+++ b/vernac/attributes.ml
@@ -339,24 +339,25 @@ let uses_parser : string key_parser = fun orig args ->
 
 let using = attribute_of_list ["using",uses_parser]
 
-let process_typing_att ~typing_flags att enable =
+let process_typing_att ~typing_flags att disable =
+  let enable = not disable in
   match att with
   | "universes" ->
     { typing_flags with
       Declarations.check_universes = enable
     }
-  | "guarded" ->
+  | "guard" ->
     { typing_flags with
       Declarations.check_guarded = enable
     }
-  | "positive" ->
+  | "positivity" ->
     { typing_flags with
       Declarations.check_positive = enable
     }
   | att ->
     CErrors.user_err Pp.(str "Unknown “typing” attribute: " ++ str att)
 
-let process_typing_enable ~key = function
+let process_typing_disable ~key = function
   | VernacFlagEmpty | VernacFlagLeaf (FlagIdent "yes") ->
     true
   | VernacFlagLeaf (FlagIdent "no") ->
@@ -368,8 +369,8 @@ 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 enable = process_typing_enable ~key:typing_att enable in
-      let typing_flags = process_typing_att ~typing_flags typing_att enable in
+      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
@@ -380,4 +381,4 @@ let typing_flags_parser : Declarations.typing_flags key_parser = fun orig args -
     CErrors.user_err Pp.(str "Ill-formed “typing” attribute: " ++ pr_vernac_flag_value att)
 
 let typing_flags =
-  attribute_of_list ["typing", typing_flags_parser]
+  attribute_of_list ["bypass_check", typing_flags_parser]
-- 
cgit v1.2.3