From e287e4181dcd4d78df198beabe9a725e74550624 Mon Sep 17 00:00:00 2001 From: Pierre Rousselin Date: Sun, 4 Aug 2024 12:41:52 +0200 Subject: [PATCH] Add links to refman in test files The goal is to ease maintenance if one of the test files fails following a change in some command behaviour regarding locality. --- .../success/locality_attributes_modules.v | 18 +++++++++++++++++- .../locality_attributes_modules_ltac2.v | 18 +++++++++++++++++- .../success/locality_attributes_sections.v | 19 ++++++++++++++++++- .../locality_attributes_sections_in_modules.v | 19 ++++++++++++++++++- .../locality_attributes_sections_ltac2.v | 19 ++++++++++++++++++- 5 files changed, 88 insertions(+), 5 deletions(-) diff --git a/test-suite/success/locality_attributes_modules.v b/test-suite/success/locality_attributes_modules.v index 35c38dd33883..a06a77c51c0d 100644 --- a/test-suite/success/locality_attributes_modules.v +++ b/test-suite/success/locality_attributes_modules.v @@ -1,7 +1,23 @@ (** This file tests how locality attributes affect usual vernacular commands. PLEASE, when this file fails to compute following a voluntary change in Coq's behaviour, modify accordingly the tables in [sections.rst] and - [modules.rst] in [doc/sphinx/language/core] *) + [modules.rst] in [doc/sphinx/language/core]. + + Also look at the corresponding discussions about locality attributes in the + refman (directory doc/sphinx) + - For Definition, Lemma, ..., look at language/core/definitions.rst + - For Axiom, Conjecture, ..., look at language/core/assumptions.rst + - For abbreviations, look at user-extensions/syntax-extensions.rst + - For Notations, look at user-extensions/syntax-extensions.rst + - For Tactic Notations, look at user-extensions/syntax-extensions.rst + - For Ltac, look at proof-engine/ltac.rst + - For Canonical Structures, look at language/extensions/canonical.rst + - For Hints, look at proofs/automatic-tactics/auto.rst + - For Coercions, look at addendum/implicit-coercions.rst + - For Ltac2, look at proof-engine/ltac2.rst + - For Ltac2 Notations, look at proof-engine/ltac2.rst + - For Set, look at language/core/basic.rst +*) (** This structure is used to test availability or not of a [Canonical Structure]. *) diff --git a/test-suite/success/locality_attributes_modules_ltac2.v b/test-suite/success/locality_attributes_modules_ltac2.v index 031bc99927b4..4ca1a34607c2 100644 --- a/test-suite/success/locality_attributes_modules_ltac2.v +++ b/test-suite/success/locality_attributes_modules_ltac2.v @@ -1,7 +1,23 @@ (** This file tests how locality attributes affect usual vernacular commands. PLEASE, when this file fails to compute following a voluntary change in Coq's behaviour, modify accordingly the tables in [sections.rst] and - [modules.rst] in [doc/sphinx/language/core] *) + [modules.rst] in [doc/sphinx/language/core] + + Also look at the corresponding discussions about locality attributes in the + refman (directory doc/sphinx) + - For Definition, Lemma, ..., look at language/core/definitions.rst + - For Axiom, Conjecture, ..., look at language/core/assumptions.rst + - For abbreviations, look at user-extensions/syntax-extensions.rst + - For Notations, look at user-extensions/syntax-extensions.rst + - For Tactic Notations, look at user-extensions/syntax-extensions.rst + - For Ltac, look at proof-engine/ltac.rst + - For Canonical Structures, look at language/extensions/canonical.rst + - For Hints, look at proofs/automatic-tactics/auto.rst + - For Coercions, look at addendum/implicit-coercions.rst + - For Ltac2, look at proof-engine/ltac2.rst + - For Ltac2 Notations, look at proof-engine/ltac2.rst + - For Set, look at language/core/basic.rst +*) From Ltac2 Require Import Ltac2. diff --git a/test-suite/success/locality_attributes_sections.v b/test-suite/success/locality_attributes_sections.v index 5cf805f5f833..e2a695feb157 100644 --- a/test-suite/success/locality_attributes_sections.v +++ b/test-suite/success/locality_attributes_sections.v @@ -1,7 +1,24 @@ (** This file tests how locality attributes affect usual vernacular commands. PLEASE, when this file fails to compute following a voluntary change in Coq's behaviour, modify accordingly the tables in [sections.rst] and - [modules.rst] in [doc/sphinx/language/core] *) + [modules.rst] in [doc/sphinx/language/core]. + + Also look at the corresponding discussions about locality attributes in the + refman (directory doc/sphinx) + - For Definition, Lemma, ..., look at language/core/definitions.rst + - For Axiom, Conjecture, ..., look at language/core/assumptions.rst + - For abbreviations, look at user-extensions/syntax-extensions.rst + - For Notations, look at user-extensions/syntax-extensions.rst + - For Tactic Notations, look at user-extensions/syntax-extensions.rst + - For Ltac, look at proof-engine/ltac.rst + - For Canonical Structures, look at language/extensions/canonical.rst + - For Hints, look at proofs/automatic-tactics/auto.rst + - For Coercions, look at addendum/implicit-coercions.rst + - For Ltac2, look at proof-engine/ltac2.rst + - For Ltac2 Notations, look at proof-engine/ltac2.rst + - For Set, look at language/core/basic.rst +*) + (** This structure is used to test availability or not of a [Canonical Structure]. *) diff --git a/test-suite/success/locality_attributes_sections_in_modules.v b/test-suite/success/locality_attributes_sections_in_modules.v index 3c8aa0ec3af0..4b305605b691 100644 --- a/test-suite/success/locality_attributes_sections_in_modules.v +++ b/test-suite/success/locality_attributes_sections_in_modules.v @@ -1,7 +1,24 @@ (** This file tests how locality attributes affect usual vernacular commands. PLEASE, when this file fails to compute following a voluntary change in Coq's behaviour, modify accordingly the tables in [sections.rst] and - [modules.rst] in [doc/sphinx/language/core] *) + [modules.rst] in [doc/sphinx/language/core]. + + Also look at the corresponding discussions about locality attributes in the + refman (directory doc/sphinx) + - For Definition, Lemma, ..., look at language/core/definitions.rst + - For Axiom, Conjecture, ..., look at language/core/assumptions.rst + - For abbreviations, look at user-extensions/syntax-extensions.rst + - For Notations, look at user-extensions/syntax-extensions.rst + - For Tactic Notations, look at user-extensions/syntax-extensions.rst + - For Ltac, look at proof-engine/ltac.rst + - For Canonical Structures, look at language/extensions/canonical.rst + - For Hints, look at proofs/automatic-tactics/auto.rst + - For Coercions, look at addendum/implicit-coercions.rst + - For Ltac2, look at proof-engine/ltac2.rst + - For Ltac2 Notations, look at proof-engine/ltac2.rst + - For Set, look at language/core/basic.rst +*) + (** This structure is used to test availability or not of a [Canonical Structure]. *) diff --git a/test-suite/success/locality_attributes_sections_ltac2.v b/test-suite/success/locality_attributes_sections_ltac2.v index dd43c9188432..141497f63917 100644 --- a/test-suite/success/locality_attributes_sections_ltac2.v +++ b/test-suite/success/locality_attributes_sections_ltac2.v @@ -1,7 +1,24 @@ (** This file tests how locality attributes affect usual vernacular commands. PLEASE, when this file fails to compute following a voluntary change in Coq's behaviour, modify accordingly the tables in [sections.rst] and - [modules.rst] in [doc/sphinx/language/core] *) + [modules.rst] in [doc/sphinx/language/core]. + + Also look at the corresponding discussions about locality attributes in the + refman (directory doc/sphinx) + - For Definition, Lemma, ..., look at language/core/definitions.rst + - For Axiom, Conjecture, ..., look at language/core/assumptions.rst + - For abbreviations, look at user-extensions/syntax-extensions.rst + - For Notations, look at user-extensions/syntax-extensions.rst + - For Tactic Notations, look at user-extensions/syntax-extensions.rst + - For Ltac, look at proof-engine/ltac.rst + - For Canonical Structures, look at language/extensions/canonical.rst + - For Hints, look at proofs/automatic-tactics/auto.rst + - For Coercions, look at addendum/implicit-coercions.rst + - For Ltac2, look at proof-engine/ltac2.rst + - For Ltac2 Notations, look at proof-engine/ltac2.rst + - For Set, look at language/core/basic.rst +*) + From Ltac2 Require Import Ltac2.