Skip to content

Commit f4532a8

Browse files
committed
remove a wrong quote character
1 parent 0eddf17 commit f4532a8

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)