| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
multiple pages.
Reviewed-by: jfehrle
|
|
Reviewed-by: JasonGross
Ack-by: Zimmi48
Ack-by: herbelin
|
|
|
|
|
|
|
|
Co-Authored-By: Théo Zimmermann <theo.zimmi@gmail.com>
|
|
Useful for guarding calls to `unfold` or `cbv` to ensure that, e.g.,
`Opaque foo` doesn't break some automation which tries to unfold `foo`.
We have some timeouts in the strategy success file. We should not run
into issues, because we are not really testing how long these take. We
could just as well use `Timeout 60` or longer, we just want to make sure
the file dies more quickly rather than taking over 10^100 steps.
Note that this tactic does not play well with `abstract`; I have a
potentially controversial change that fixes this issue.
One of the lines in the doc comes from
https://github.com/coq/coq/pull/12129#issuecomment-619771556
Co-Authored-By: Pierre-Marie Pédrot <pierre-marie.pedrot@irif.fr>
Co-Authored-By: Théo Zimmermann <theo.zimmermann@inria.fr>
Co-Authored-By: Michael Soegtrop <7895506+MSoegtropIMC@users.noreply.github.com>
|
|
|
|
|
|
Ack-by: JasonGross
Ack-by: Zimmi48
Ack-by: cpitclaudel
|
|
|
|
Reviewed-by: jfehrle
|
|
|
|
|
|
|
|
Co-Authored-By: Théo Zimmermann <theo.zimmi@gmail.com>
|
|
Ack-by: SkySkimmer
Ack-by: Zimmi48
|
|
|
|
Reviewed-by: ejgallego
|
|
|
|
|
|
|
|
We do two changes:
- We distinguish between a notion of format generically attached to
notations and a new notion of format attached to interpreted
notations. "Reserved Notation" attaches a format
generically. "Notation" attaches the format specifically to the given
interpretation, and additionally, attaches it generically if it is the
first time the notation is defined.
- We warn before overriding an explicitly reserved generic format, or
a specific format.
|
|
If it is for an internal non-terminal then:
- if for a subentry different from constr, it refers to the head of
the subentry
- if in constr, it is 200 by convention
If it is on the border of a rule, then:
- if it is in a subentry different from the entry it lives, it refers
to the head of the subentry (or 200 by convention if in constr)
- if it is in the same entry, the rule for associativity tells if a
SELF, a NEXT, or (if on the right) a LEVEL
|
|
Update doc_grammar tool
The grammar in the doc is generated semi-automatically with doc_grammar:
- the grammar is automatically extracted from the mlg files
- developer-prepared editing scripts *.mlg_edit modify the extracted
grammar for clarity, simplicity and ordering of productions
- chunks of the resulting grammar are automatically inserted into the
rsts using instructions embedded in the rsts
Running doc_grammar is currently a manual step.
The grammar updates in the rst files have been manually reviewed.
|
|
|
|
|
|
|
|
document « Property »
more documentation fixes
[doc] destructed → destructured
[doc] another le_minus→lt_1_r
[doc] @jfehrle suggestions
[doc] more minor fixes
|
|
This is to prevent confusion with the terminology used in the grammar
of tactic in the reference manual: "intropattern" in Tactic Notation
and TACTIC EXTEND is actually bound to simple_intropattern and not to
what is called intropattern in the reference manual
After some deprecation phase, "intropattern" could be added back to
mean the "intropattern" of the reference manual.
Note that "simple_intropattern" is actually already available in
"Tactic Notation" with the correct meaning as an entry. Only
"intropattern" is misguiding.
|
|
Ack-by: SkySkimmer
Ack-by: Zimmi48
Reviewed-by: ejgallego
Ack-by: ggonthier
Reviewed-by: herbelin
Ack-by: jfehrle
Reviewed-by: mattam82
|
|
Ack-by: JasonGross
Reviewed-by: SkySkimmer
Reviewed-by: cpitclaudel
|
|
* use mixfix `(p1 | … | pn)` notation for nested disjunctive patterns,
rather than infix `|`, making pattern syntax consistent with term
syntax.
* disable extending `pattern` grammar with notation incompatible with
the nested disjunctive pattern syntax `(p1 | … | pn)`, such as the `(p
| q)` divisibility notation used by `Numbers`.
* emit a (disabled by default) `disj-pattern-notation` warning when such
`Notation` is attempted.
* update documentation accordingly; document incompatibilities in
`changelog`.
* comment special treatment of `(num)` in grammar.
* update file extensions in `Pcoq` header comment.
* correct the keyword declarations to reflect the contents of the
grammar files; perhaps there should be an option to disable implicit
keyword extension in a `.mlg` file, so that these lists could actually
be checked.
* parse the `|}` manifest record terminator as `|` followed by `}`,
eliminating the `|}` token which conflicts with notations that use `|`
as a terminator (such as, absolute value, norm, or cardinal in
MathComp). Since `|` is now an `operconstr` _and_ `pattern` terminator,
`bar_cbrace` rule checks for contiguous symbols, this change entails no
visible behaviour change.
|
|
Co-Authored-By: Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr>
|
|
Co-Authored-By: Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr>
|
|
Co-Authored-By: Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr>
|
|
Progress towards #9411, extracted from #10118, rebased ontop of #10192.
|
|
3d09e39dd423d81c6af3e991d5b282ea8608646b
The commit mentioned above changed the semantics of `Bind Scope` to
a dynamic binding behavior. It forgot to update the documentation.
Fixes #10064
|
|
Co-Authored-By: @Zimmi48
|
|
|
|
|
|
Co-Authored-By: Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr>
|
|
|
|
|
|
Add more links to PRs and credits of authors.
|
|
|
|
Reviewed-by: Zimmi48
Reviewed-by: ejgallego
Ack-by: gares
Ack-by: herbelin
Ack-by: ppedrot
Ack-by: proux01
|
|
|
