Skip to content

Instantly share code, notes, and snippets.

@Blaisorblade

Blaisorblade/hide_global_hints.v

Created February 26, 2022 00:51
Show Gist options
  • Save Blaisorblade/9a33fa9afcf58e499ab097f596a9d901 to your computer and use it in GitHub Desktop.
Save Blaisorblade/9a33fa9afcf58e499ab097f596a9d901 to your computer and use it in GitHub Desktop.
Download ZIP
Coq: Opaque module ascription already hides global hints
Raw
hide_global_hints.v
Require Import stdpp.base.
Module Type FOO.
Definition number : Set := nat.
End FOO.
Module Import foo : FOO.
Definition number : Set := nat.
Fail #[global] Instance number_inh : Inhabited number := _.
Require stdpp.numbers.
#[global] Instance number_inh : Inhabited number := _.
End foo.
Fail #[global] Instance: Inhabited number := _.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment