The Coq mailing list

[jonikelee <jonikelee AT comcast.net>]

I'm not sure if I'm hitting a bug or being told something is not legal Coq.

I have a Section with Contexts, a rewrite rule defined there, and an attempt to add a hint for that rewrite after the section.  Like this:

Section defs.
  Context {A : Type}.
  Context {ordA : Ordered A}.
  ...
  Lemma my_rw_rule : ...
End defs.

Hint Rewrite my_rw_rule : rw_rules.

The above Hint Rewrite produces the following error:

Toplevel input, characters 0-34:
Error:
Unable to satisfy the following constraints:

?1 : "Type"
?2 : "Ordered ?1"

Obviously, those constraints can't be solved outside that Section - but they can be solve elsewhere (other similarly contextualized sections, etc.).  And, Hints added in the section don't survive the end of the section.  Also note that Hint Resolve after the section for things defined in that section doesn't produce any such error.   If Hint Resolve knows enough to delay attempting to satisfy those constraints until the rule is applied, why doesn't Hint Rewrite?

Do I need to handle rewrite rules defined under Contexts differently?

-- Jonathan