[attributes] [typing] Rename typing to bypass_check

As discussed in the Coq meeting.

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::
 

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:

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
 

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
 

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 *)

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]