diff options
| -rw-r--r-- | doc/sphinx/language/core/coinductive.rst | 4 | ||||
| -rw-r--r-- | doc/sphinx/language/core/definitions.rst | 6 | ||||
| -rw-r--r-- | doc/sphinx/language/core/inductive.rst | 12 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/vernacular-commands.rst | 18 | ||||
| -rw-r--r-- | test-suite/success/typing_flags.v | 26 | ||||
| -rw-r--r-- | 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] |