From 61c780ad8138bfa768977d652c25741dad35d448 Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Thu, 18 Apr 2019 14:26:39 +0200 Subject: First fixing pass, and experiment with dune-style PR number and author listing. --- doc/sphinx/language/gallina-extensions.rst | 1 + 1 file changed, 1 insertion(+) (limited to 'doc/sphinx/language') diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst index 695dea222f..5308330820 100644 --- a/doc/sphinx/language/gallina-extensions.rst +++ b/doc/sphinx/language/gallina-extensions.rst @@ -2244,6 +2244,7 @@ Printing universes unspecified if `string` doesn’t end in ``.dot`` or ``.gv``. .. cmdv:: Print Universes Subgraph(@names) + :name: Print Universes Subgraph Prints the graph restricted to the requested names (adjusting constraints to preserve the implied transitive constraints between -- cgit v1.2.3 From 4895bf8bb5d0acfaee499991973fc6537657427d Mon Sep 17 00:00:00 2001 From: Vincent Laporte Date: Fri, 10 May 2019 08:48:54 +0000 Subject: [refman] Mention the `#[canonical(false)]` attribute --- doc/sphinx/language/gallina-extensions.rst | 19 +++++++++++++++++++ 1 file changed, 19 insertions(+) (limited to 'doc/sphinx/language') diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst index 5308330820..ba766c8c3d 100644 --- a/doc/sphinx/language/gallina-extensions.rst +++ b/doc/sphinx/language/gallina-extensions.rst @@ -2048,6 +2048,21 @@ in :ref:`canonicalstructures`; here only a simple example is given. If a same field occurs in several canonical structures, then only the structure declared first as canonical is considered. + .. note:: + To prevent a field from being involved in the inference of canonical instances, + its declaration can be annotated with the :g:`#[canonical(false)]` attribute. + + .. example:: + + For instance, when declaring the :g:`Setoid` structure above, the + :g:`Prf_equiv` field declaration could be written as follows. + + .. coqdoc:: + + #[canonical(false)] Prf_equiv : equivalence Carrier Equal + + See :ref:`canonicalstructures` for a more realistic example. + .. cmdv:: Canonical {? Structure } @ident {? : @type } := @term This is equivalent to a regular definition of :token:`ident` followed by the @@ -2067,6 +2082,10 @@ in :ref:`canonicalstructures`; here only a simple example is given. Print Canonical Projections. + .. note:: + + The last line would not show up if the corresponding projection (namely + :g:`Prf_equiv`) were annotated as not canonical, as described above. Implicit types of variables ~~~~~~~~~~~~~~~~~~~~~~~~~~~ -- cgit v1.2.3 From feb9c50b5812a01e9dc60e2408f4f9f38986ce8c Mon Sep 17 00:00:00 2001 From: Clément Pit-Claudel Date: Fri, 10 May 2019 22:29:57 -0400 Subject: [refman] Introduce syntax for alternatives in notations Closes GH-8482. --- doc/sphinx/language/gallina-extensions.rst | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) (limited to 'doc/sphinx/language') diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst index 5308330820..af658b4698 100644 --- a/doc/sphinx/language/gallina-extensions.rst +++ b/doc/sphinx/language/gallina-extensions.rst @@ -931,7 +931,7 @@ In the syntax of module application, the ! prefix indicates that any :token:`module_binding`. The output module type is verified against each :token:`module_type`. -.. cmdv:: Module [ Import | Export ] +.. cmdv:: Module {| Import | Export } Behaves like :cmd:`Module`, but automatically imports or exports the module. @@ -1648,7 +1648,7 @@ Declaring Implicit Arguments -.. cmd:: Arguments @qualid {* [ @ident ] | { @ident } | @ident } +.. cmd:: Arguments @qualid {* {| [ @ident ] | { @ident } | @ident } } :name: Arguments (implicits) This command is used to set implicit arguments *a posteriori*, @@ -1665,20 +1665,20 @@ Declaring Implicit Arguments This command clears implicit arguments. -.. cmdv:: Global Arguments @qualid {* [ @ident ] | { @ident } | @ident } +.. cmdv:: Global Arguments @qualid {* {| [ @ident ] | { @ident } | @ident } } This command is used to recompute the implicit arguments of :token:`qualid` after ending of the current section if any, enforcing the implicit arguments known from inside the section to be the ones declared by the command. -.. cmdv:: Local Arguments @qualid {* [ @ident ] | { @ident } | @ident } +.. cmdv:: Local Arguments @qualid {* {| [ @ident ] | { @ident } | @ident } } When in a module, tell not to activate the implicit arguments of :token:`qualid` declared by this command to contexts that require the module. -.. cmdv:: {? Global | Local } Arguments @qualid {*, {+ [ @ident ] | { @ident } | @ident } } +.. cmdv:: {? {| Global | Local } } Arguments @qualid {*, {+ {| [ @ident ] | { @ident } | @ident } } } For names of constants, inductive types, constructors, lemmas which can only be applied to a fixed number of @@ -2148,7 +2148,7 @@ that specify which variables should be generalizable. Disable implicit generalization entirely. This is the default behavior. -.. cmd:: Generalizable (Variable | Variables) {+ @ident } +.. cmd:: Generalizable {| Variable | Variables } {+ @ident } Allow generalization of the given identifiers only. Calling this command multiple times adds to the allowed identifiers. -- cgit v1.2.3 From 942621f7747bd56a7da35cacc21f0e5fdbf93413 Mon Sep 17 00:00:00 2001 From: Clément Pit-Claudel Date: Sun, 12 May 2019 19:38:36 -0400 Subject: [refman] Misc fixes (indentation, whitespace, notation syntax) --- doc/sphinx/language/gallina-extensions.rst | 10 ++++----- .../language/gallina-specification-language.rst | 26 +++++++++++----------- 2 files changed, 18 insertions(+), 18 deletions(-) (limited to 'doc/sphinx/language') diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst index ccd25ec9f3..96e74bf118 100644 --- a/doc/sphinx/language/gallina-extensions.rst +++ b/doc/sphinx/language/gallina-extensions.rst @@ -831,16 +831,16 @@ Sections create local contexts which can be shared across multiple definitions. Links :token:`type` to each :token:`ident`. - .. cmdv:: Variable {+ ( {+ @ident } : @type ) } + .. cmdv:: Variable {+ ( {+ @ident } : @type ) } Declare one or more variables with various types. - .. cmdv:: Variables {+ ( {+ @ident } : @type) } - Hypothesis {+ ( {+ @ident } : @type) } - Hypotheses {+ ( {+ @ident } : @type) } + .. cmdv:: Variables {+ ( {+ @ident } : @type) } + Hypothesis {+ ( {+ @ident } : @type) } + Hypotheses {+ ( {+ @ident } : @type) } :name: Variables; Hypothesis; Hypotheses - These variants are synonyms of :n:`Variable {+ ( {+ @ident } : @type) }`. + These variants are synonyms of :n:`Variable {+ ( {+ @ident } : @type) }`. .. cmd:: Let @ident := @term diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/gallina-specification-language.rst index 5a1af9f9fa..8acbcbec8f 100644 --- a/doc/sphinx/language/gallina-specification-language.rst +++ b/doc/sphinx/language/gallina-specification-language.rst @@ -616,34 +616,34 @@ has type :token:`type`. Adds several parameters with specification :token:`type`. - .. cmdv:: Parameter {+ ( {+ @ident } : @type ) } + .. cmdv:: Parameter {+ ( {+ @ident } : @type ) } Adds blocks of parameters with different specifications. - .. cmdv:: Local Parameter {+ ( {+ @ident } : @type ) } + .. cmdv:: Local Parameter {+ ( {+ @ident } : @type ) } :name: Local Parameter Such parameters are never made accessible through their unqualified name by :cmd:`Import` and its variants. You have to explicitly give their fully qualified name to refer to them. - .. cmdv:: {? Local } Parameters {+ ( {+ @ident } : @type ) } - {? Local } Axiom {+ ( {+ @ident } : @type ) } - {? Local } Axioms {+ ( {+ @ident } : @type ) } - {? Local } Conjecture {+ ( {+ @ident } : @type ) } - {? Local } Conjectures {+ ( {+ @ident } : @type ) } + .. cmdv:: {? Local } Parameters {+ ( {+ @ident } : @type ) } + {? Local } Axiom {+ ( {+ @ident } : @type ) } + {? Local } Axioms {+ ( {+ @ident } : @type ) } + {? Local } Conjecture {+ ( {+ @ident } : @type ) } + {? Local } Conjectures {+ ( {+ @ident } : @type ) } :name: Parameters; Axiom; Axioms; Conjecture; Conjectures - These variants are synonyms of :n:`{? Local } Parameter {+ ( {+ @ident } : @type ) }`. + These variants are synonyms of :n:`{? Local } Parameter {+ ( {+ @ident } : @type ) }`. - .. cmdv:: Variable {+ ( {+ @ident } : @type ) } - Variables {+ ( {+ @ident } : @type ) } - Hypothesis {+ ( {+ @ident } : @type ) } - Hypotheses {+ ( {+ @ident } : @type ) } + .. cmdv:: Variable {+ ( {+ @ident } : @type ) } + Variables {+ ( {+ @ident } : @type ) } + Hypothesis {+ ( {+ @ident } : @type ) } + Hypotheses {+ ( {+ @ident } : @type ) } :name: Variable (outside a section); Variables (outside a section); Hypothesis (outside a section); Hypotheses (outside a section) Outside of any section, these variants are synonyms of - :n:`Local Parameter {+ ( {+ @ident } : @type ) }`. + :n:`Local Parameter {+ ( {+ @ident } : @type ) }`. For their meaning inside a section, see :cmd:`Variable` in :ref:`section-mechanism`. -- cgit v1.2.3 From 4a69c594b484cb7e9af28b8ba9608a228e2376f1 Mon Sep 17 00:00:00 2001 From: Clément Pit-Claudel Date: Thu, 16 May 2019 11:00:05 -0400 Subject: [refman] Fix up the grammar entry for field_def --- doc/sphinx/language/gallina-extensions.rst | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'doc/sphinx/language') diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst index 96e74bf118..5e214f6f7f 100644 --- a/doc/sphinx/language/gallina-extensions.rst +++ b/doc/sphinx/language/gallina-extensions.rst @@ -85,7 +85,7 @@ To build an object of type :token:`ident`, one should provide the constructor .. productionlist:: record_term : {| [`field_def` ; … ; `field_def`] |} - field_def : name [binders] := `record_term` + field_def : `ident` [`binders`] := `term` Alternatively, the following syntax allows creating objects by using named fields, as shown in this grammar. The fields do not have to be in any particular order, nor do they have -- cgit v1.2.3