I have not quite followed what the various recent pull requests about plugins and parsers entail, but are they supposed to fix the following issue? (Script is currently accepted, should be rejected.)
Require ssreflect.
Goal True -> True.
idtac => H.
Why should it be rejected?
Because just requiring ssreflect
(possibly indirectly) should not modify the vanilla parser.
How should it be modified then?
When doing Import ssreflect
.
I think that what you say is more true wrt tactic names than notations (whatever that means).
But I agree it is a bug, dunno how easy it is to fix.
I mean, there are some chances that have
is not in scope ;-)
IIRC =>
is injected directly in the grammar, while have
goes trough the tactic extension mechanism, which should honor Import
Yes, there is a strange mix of both grammars. For example, it does not recognize the intro pattern //
, but with a twist:
Syntax error: [ast_closure_term] expected after '/' (in [ssrfwdview]).
Guillaume Melquiond said:
I have not quite followed what the various recent pull requests about plugins and parsers entail, but are they supposed to fix the following issue? (Script is currently accepted, should be rejected.)
Require ssreflect. Goal True -> True. idtac => H.
no, they don't change that plugins act at Require time not Import time
Guillaume Melquiond said:
Yes, there is a strange mix of both grammars. For example, it does not recognize the intro pattern
//
, but with a twist:Syntax error: [ast_closure_term] expected after '/' (in [ssrfwdview]).
probably because ssr has a hack to avoid changing the keywords at Require time
I see. As long as Reserved Notation "//"
has not been evaluated, the tokenizer does not recognize it as a token, and thus neither does SSReflect.
Last updated: Oct 13 2024 at 01:02 UTC