| Age | Commit message (Collapse) | Author |
|---|
|
only-printing notations
Reviewed-by: SkySkimmer
|
|
|
|
|
|
|
|
|
|
The (old) original model for notations was to associated both a
parsing and a printing rule to a notation.
Progressively, it become more and more common to have only parsing
notations or even multiple expressions printed with the same notation.
The new model is to attach to a given scope, string and entry at most
one either only-parsing or mixed-parsing-printing rules + an
arbitrarily many unrelated only-printing rules.
Additionally, we anticipate the ability to selectively
activate/deactivate each of those.
This allows to fix in particular #9682 but also to have
more-to-the-point warnings in case a notation overrides or partially
overrides another one.
Rules for importing are not changed (see forthcoming #12984 though).
We also improve the output of "Print Scopes" so that it adds when a
notation is only-parsing, only-printing, or deactivated, or a
combination of those.
Fixes #4738
Fixes #9682
Fixes part 2 of #12908
Fixes #13112
|
|
This is in anticipation of a model with an explicit difference between
a parsing-printing notation and the pair of only-parsing notation +
only-printing notation.
|
|
Also add optimisation of interpretation_eq.
|
|
This is to be consistent with the use of parentheses in the syntax of
Notation and to support a list of attribute afterwards.
|
|
Reviewed-by: SkySkimmer
|
|
Reviewed-by: SkySkimmer
Reviewed-by: ppedrot
Reviewed-by: ejgallego
|
|
|
|
The current implementation of par: is still in the STM, but is optional.
If the STM does not take over it, it defaults to the implementation of
in comTactic which is based on all: (i.e. sequential).
This commit also moved the interpretation of a tactic from g_ltac to
vernac/comTactic which is more appropriate.
Co-authored-by: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
|
|
Reviewed-by: ejgallego
Reviewed-by: silene
|
|
|
|
Reviewed-by: ppedrot
|
|
|
|
An h-box inhibits the breaking semantics of any cut/spc/brk in the
enclosed box.
We tentatively replace its occurrence by an h or hv, assuming in
particular that if the indentation is not 0, an hv box was intended.
|
|
|
|
specific format.
Reviewed-by: ejgallego
|
|
Reviewed-by: SkySkimmer
|
|
|
|
Reviewed-by: ppedrot
|
|
Evarconv.apply_on_subterm
Reviewed-by: mattam82
|
|
Reviewed-by: ppedrot
|
|
Reviewed-by: ppedrot
|
|
I know higher-order mutable state shared across call sites is a staple of
Matthieu's style, but it is a footgun begging to be abused.
|
|
Instead of repeatedly checking for evars to appear in a term, we perform
the search in one single pass. This slowdown was observed in fiat-crypto.
This is still a naive algorithm though, since we recompute the set of evars
for each subterm. This is thus quadratic.
|
|
Reviewed-by: jfehrle
Ack-by: ppedrot
|
|
|
|
|
|
-> "constr"
Reviewed-by: herbelin
Ack-by: Zimmi48
|
|
|
|
Reviewed-by: Zimmi48
Reviewed-by: gares
Reviewed-by: maximedenes
Reviewed-by: Matafou
Ack-by: ejgallego
|
|
Reviewed-by: jfehrle
Ack-by: Blaisorblade
Ack-by: herbelin
|
|
Update doc/sphinx/language/core/primitive.rst
Co-authored-by: Jim Fehrle <jim.fehrle@gmail.com>
Add persistent data structure
Update doc/sphinx/language/core/primitive.rst
Co-authored-by: Hugo Herbelin <herbelin@users.noreply.github.com>
Update doc/sphinx/language/core/primitive.rst
Co-authored-by: Jim Fehrle <jim.fehrle@gmail.com>
Update doc/sphinx/language/core/primitive.rst
Co-authored-by: Jim Fehrle <jim.fehrle@gmail.com>
|
|
Reviewed-by: SkySkimmer
Reviewed-by: Zimmi48
Ack-by: jfehrle
|
|
I believe this renaming makes it easier for new contributors to discover
the code of `ring`.
|
|
Reviewed-by: SkySkimmer
|
|
Reviewed-by: ejgallego
|
|
Reviewed-by: ejgallego
|
|
Reviewed-by: ejgallego
|
|
Reviewed-by: SkySkimmer
|
|
|
|
Fix #13045
Also make sure future anomalies won't be fed to tclzero.
Instead of retyping with lax:true we may question why we produce an
ill-typed term in decompose_app_rel: in the
| App (f, [|arg|]) ->
case we produce `fun x y : T => bla x y` but we have no assurance that
the second argument of `bla` should have type `T`.
|
|
Reviewed-by: ppedrot
|
|
incompatible candidates
Reviewed-by: ppedrot
|
|
|
|
It was not documented, not properly tested and thus likely buggy. Judging
from the code alone I spotted already one potential bug. Further more it was
prominently making use of the infamous "arbitrary term as hint" feature.
Since the only user in our CI seems to be a math-classes file that introduced
the feature under a claim of "cleanup", I believe we can safely remove it
without anyone noticing.
|
|
Fix #12917
|
