Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Problem with scopes

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Problem with scopes


Chronological Thread 
  • From: Pierre Courtieu <pierre.courtieu AT gmail.com>
  • To: Coq Club <coq-club AT inria.fr>
  • Subject: Re: [Coq-Club] Problem with scopes
  • Date: Wed, 24 Aug 2016 11:38:39 +0200
  • Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=pierre.courtieu AT gmail.com; spf=Pass smtp.mailfrom=pierre.courtieu AT gmail.com; spf=None smtp.helo=postmaster AT mail-lf0-f48.google.com
  • Ironport-phdr: 9a23:qSrFMBbGMq13W3cLvugwthf/LSx+4OfEezUN459isYplN5qZpcW/bnLW6fgltlLVR4KTs6sC0LuP9fu+EjRbqdbZ6TZZIcQKD0dEwewt3CUYSPafDkP6KPO4JwcbJ+9lEGFfwnegLEJOE9z/bVCB6le77DoVBwmtfVEtfre9JIfegoyN2vyo/NWLOkMT1WP7Ou05dE7+7V2I8JJH2c06cud54yCKi0MAQ/5Ry2JsKADbtDfHzeD0wqRe9T9Nsekq7c9KXPayVa05SbtFEGZuaDhtt4XD/CPORgqX53YaTn5e0l8RW1CEv1nGWcLatTKyne5g0mHONsrvCLswRD6K7qFxSRauhj1RZBAj92SCss19lrhW6DmmugZjwoPJKNWNNfdkZK6bdtQHX3ZAU9t5WClIA4f6ZIwKWblSdd1EppXw8gNd5SC1AhOhUaa2kmdF
2016-08-23 18:49 GMT+02:00 Guillaume Melquiond
<guillaume.melquiond AT inria.fr>:
> While I might get convinced that it would be better to start looking for
> a notation using the scopes that are currently stacked (before looking
> into other scopes), I would not go as far as qualifying this behavior as
> "intuitive".
>
> The current behavior is more or less to select the most recent notation.
> In particular, if there is a notation in the current file, it will take
> precedence over notations defined in other files. It seems about as
> intuitive to me as what you suggest.

Right. But having no way to modify this printing precedence is
strange. So either we link the "%" precedence with the printing one,
either we have a second precedence stack for printing.

Best
P.

Archive powered by MHonArc 2.6.18.

Top of Page