| Age | Commit message (Collapse) | Author |
|---|
|
|
|
Warnings are handled as injection commands, interleaved with options
and requires. Native compiler impacts require, so we must convert
"yes" to "no" before handling injections. As such the semantic
handling of the native command line argument must be separated from
the emission of the warning message, which this PR implements.
Fix #13819
In principle the other 2 cwarning in coqargs
(deprecated spropcumul and inputstate) should be moved to injections
too, but since they're deprecated I can't be bothered.
|
|
Also added a generic way of temporarily disabling a warning.
Also added try_finalize un lib/utils.ml.
|
|
Reviewed-by: SkySkimmer
Reviewed-by: Zimmi48
|
|
|
|
inductive definitions.
Reviewed-by: SkySkimmer
|
|
Ack-by: SkySkimmer
Reviewed-by: ppedrot
|
|
Also works for simpl.
|
|
|
|
|
|
Destruct has changed semantics, but I'd like to see how CI fares so far.
|
|
notations.
Reviewed-by: jfehrle
Reviewed-by: proux01
Ack-by: Zimmi48
Ack-by: SkySkimmer
|
|
Also includes some fine-tuning of error messages.
|
|
We also simplify the whole process of interpretation of cases pattern
on the way.
|
|
Fix #13595
|
|
Reviewed-by: Zimmi48
Ack-by: jfehrle
|
|
|
|
Reviewed-by: ppedrot
|
|
This avoids doing it repeatedly for nothing in intern/extern.
|
|
- float and array values are now supported for printing and parsing in custom notations (and in notations defined using the ocaml API)
- the three constants bound to the primitive float, int and array type are now allowed anywhere inside a term to print, to handle them similar to `real` type constructors
- Grants #13484: String notations for primitive arrays
- Fixes #13517: String notation printing fails with primitive integers inside lists
|
|
Ack-by: SkySkimmer
Ack-by: ppedrot
Reviewed-by: vbgl
|
|
Following a request from Pierre-Marie Pédrot in #13258
|
|
|
|
Reviewed-by: gares
|
|
|
|
|
|
- rename @{u} to @{uu} (u is the default name so using @{u} doesn't
test as much as it should)
- move part of the test using Require to end of the file (when quickly
testing changes this allows to run most of the test without compiling
the Require'd file)
|
|
coercion not being used
Reviewed-by: ejgallego
|
|
|
|
In #11172, an "=" on the number of arguments of an applied coercion
had become a ">" on the number of arguments of the coercion. It should
have been a ">=". The rest of changes in constrextern.ml is "cosmetic".
Note that in #11172, in the case of a coercion to funclass, the
definition of number of arguments of an applied coercion had moved
from including the extra arguments of the coercion to funclass to
exactly the nomber of arguments of the coercion (excluding the extra
arguments). This was necessary to take into account that several
coercions can be nested, at least of those involving a coercion to
funclass.
Incidentally, we create a dedicated output file for notations and
coercions.
|
|
|
|
between variable and non-qualified global references
Reviewed-by: ejgallego
Ack-by: maximedenes
Ack-by: gares
|
|
then by last imported
Reviewed-by: Zimmi48
Ack-by: RalfJung
Ack-by: gares
|
|
|
|
This allows e.g. to support a notation of the form "x <== y <== z <= t"
standing for "x <= y /\ y <= z /\ z <= t".
|
|
Reviewed-by: herbelin
|
|
|
|
This relies on finer-than partial order check with. In particular:
- number and order of notation metavariables does not matter
- take care of recursive patterns inclusion
|
|
Reviewed-by: Zimmi48
|
|
This allows to know which global references whose basename may be
unexpectedly caught need to be qualified.
Note: the alternative strategy, which is sometimes used, of renaming
the binding variables so as to avoid collisions with the basename of a
global reference is somehow less nice.
|
|
variables.
Reviewed-by: ejgallego
Ack-by: ppedrot
Ack-by: SkySkimmer
|
|
|
|
|
|
Reviewed-by: silene
Reviewed-by: gares
Reviewed-by: Zimmi48
|
|
This makes it so that we have an application `h a b` with both `a` and
`b` unbound, `a` is the one that is reported (parent commit with my current
compiler setup reports `b` first, and the code does not define which
it should be).
Ideally we would report both but that requires more code.
|
|
This is consistent with the syntax of Notation and is (IMO) clearer.
|
|
It finds "( x , y , .. , z )".
Co-authored-by: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
|
|
E.g. Locate "(x , y , .. , z )" now works while only
Locate "(_ , _ , .. , _ )" was working before.
This also fixes a confusion between a variable and its anonymization
into _, wrongly finding notations mentioning '_'.
Co-authored-by: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
|
|
handler in NotFoundInstance
Reviewed-by: ejgallego
|
|
|
