Typo in Polymorphism.v

[bkushigian]

In lines 18-22 of Polymorphism.v there is a typo describing option. I'd do a PR but I'm not quite sure what it should say:

While Java and friends force all sorts of different types to include the special value [null],
in Coq we request that option explicitly [something here] by wrapping a type in [option].

[p0llard]

I don't think this is a typo; if you replace 'that' with 'this' it might be easier to parse. The first occurrence of the word option is using it in its normal, dictionary definition sense.

[achlipala]

This could be a corner case of the way I perceive English, but the original sounds fine to me. The word "explicitly" is an adverb modifying "request."

[bkushigian]

No no, you're right, this was a parse error on my part