Skip to content

Commit 0fd71cf

Browse files
authored
Merge pull request #331 from ybertot/fix_doc_structures
remove a wrong quote character
2 parents 0eddf17 + f4532a8 commit 0fd71cf

File tree

1 file changed

+1
-1
lines changed

1 file changed

+1
-1
lines changed

structures.v

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -577,7 +577,7 @@ HB.structure Definition StructureName params :=
577577
- [#[infer(variable)]], where [variable : pT] belongs to [params] and is a structure
578578
(e.g. from the hierarchy) with a coercion/canonical projection [pT >-> Sortclass].
579579
It modifies the notation [StructureName.type] so as to accept [variable : Type] instead,
580-
and will try to infer it's [pT] by unification (using canonical structure inference),
580+
and will try to infer its [pT] by unification (using canonical structure inference),
581581
This is essential in [Lmodule.type R] where [R] should have type [Ring.type]
582582
but any [Type] which is canonically a [Ring.type] is accepted thanks to [#[infer(R)]].
583583
If the carrier of the structure [S] is not a [Type] but rather a function, one has

0 commit comments

Comments
 (0)