The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

Hi,

Is it possible to make a canonical structure instance local?  I can't use the [Local] prefix, as I get the error "Error: This command does not support the "Local" prefix.".  However, I want to trigger the instance that I have when a projection matches a section variable, and if I leave the instance in, I get unrelated canonical structure failures (and the occasional anomaly), such as the following:

Structure foo := { bar : Type; baz : bar }.

Canonical Structure foon := {| bar := nat ; baz := 0 |}.

Definition qux := nat.

Definition z : qux := 0.

Check (eq_refl : baz _ = z).

Section x.

  Variable b : Type.

  Variable p : b.

  Canonical Structure local_foo (bad : False) := {| bar := b ; baz := p |}.

End x.

Goal True.

pose (eq_refl : baz _ = z). (* Error: Cannot infer an internal placeholder of type "False". *)

Thanks,

Jason