diff options
| author | Maxime Dénès | 2019-02-13 21:53:15 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2019-02-13 21:53:15 +0100 |
| commit | 64eaf184df8ca52b7254a03e3b4f87c3c0491fdd (patch) | |
| tree | 4abe81d9b619baeeb844a3a3b653a27086ddbf67 /doc | |
| parent | aa2d7486702433c94bfd645d3a5f6575a9ee729f (diff) | |
| parent | 737ae4816a9c84369bc1c0a0b359a9fd4f63dbe6 (diff) | |
Merge PR #9450: Fix #9432: canonical structure and coercion accept universe binders.
Ack-by: SkySkimmer
Reviewed-by: Zimmi48
Ack-by: gares
Reviewed-by: maximedenes
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/sphinx/language/gallina-extensions.rst | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst index 437b8e557e..933f07674a 100644 --- a/doc/sphinx/language/gallina-extensions.rst +++ b/doc/sphinx/language/gallina-extensions.rst @@ -1924,9 +1924,10 @@ applied to an unknown structure instance (an implicit argument) and a value. The complete documentation of canonical structures can be found in :ref:`canonicalstructures`; here only a simple example is given. -.. cmd:: Canonical Structure @qualid +.. cmd:: Canonical {? Structure } @qualid - This command declares :token:`qualid` as a canonical structure. + This command declares :token:`qualid` as a canonical instance of a + structure (a record). Assume that :token:`qualid` denotes an object ``(Build_struct`` |c_1| … |c_n| ``)`` in the structure :g:`struct` of which the fields are |x_1|, …, |x_n|. @@ -1961,7 +1962,7 @@ in :ref:`canonicalstructures`; here only a simple example is given. Definition nat_setoid : Setoid := Build_Setoid eq_nat_equiv. - Canonical Structure nat_setoid. + Canonical nat_setoid. Thanks to :g:`nat_setoid` declared as canonical, the implicit arguments :g:`A` and :g:`B` can be synthesized in the next statement. @@ -1978,11 +1979,10 @@ 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. - .. cmdv:: Canonical Structure @ident {? : @type } := @term + .. cmdv:: Canonical {? Structure } @ident {? : @type } := @term This is equivalent to a regular definition of :token:`ident` followed by the - declaration :n:`Canonical Structure @ident`. - + declaration :n:`Canonical @ident`. .. cmd:: Print Canonical Projections |