Stream: Coq users

Topic: "The following term contains unresolved implicit arguments:"

view this post on Zulip Paolo Giarrusso (Dec 06 2020 at 17:40):

After switching from 8.11.2 to 8.12.1, the error text changes for things like:

Definition foo :=
  forall strict, True.

That now gives:

The following term contains unresolved implicit arguments:
  (?T → True)
More precisely:
- ?T: Cannot infer the type of strict.

I'd ?T is not an implicit argument — and with a bigger term, that might be actively misleading.

Last updated: Oct 13 2024 at 01:02 UTC