Stream: Coq users

Topic: why can't I #[export] Existing Instance

Paolo Giarrusso (Dec 10 2020 at 01:20):

Module ptr_pred_helpers.
  Fail Fail Global Existing Instance observe_strict_valid_valid.
  Fail Fail Local Existing Instance observe_strict_valid_valid.
  Fail #[export] Existing Instance observe_strict_valid_valid.
End ptr_pred_helpers.

Paolo Giarrusso (Dec 10 2020 at 01:59):

oh

  #[export] Hint Resolve observe_strict_valid_valid : typeclass_instances.

Paolo Giarrusso (Dec 10 2020 at 02:01):

ah, #[export] Instance doesn't work either

Paolo Giarrusso (Dec 10 2020 at 02:02):

this is BTW on Coq 8.12.1

Paolo Giarrusso (Dec 10 2020 at 02:10):

sorry, found https://coq.discourse.group/t/change-of-default-locality-for-hint-commands-in-coq-8-13/1140/12, and sad :-(

Théo Zimmermann (Dec 10 2020 at 08:42):

It's just a case of not implemented yet.

Christian Doczkal (Dec 10 2020 at 12:09):

Yes, this is probably another change that people supporting multiple versions of Coq will have to ignore for a while. IIRC mathcomp just dropped support for 8.7, 8.8 and 8.9, so now they can finally use Declare Scope...

Last updated: Oct 04 2023 at 19:01 UTC