| Age | Commit message (Collapse) | Author |
|---|
|
Reviewed-by: gares
Ack-by: Janno
Ack-by: CohenCyril
Ack-by: Zimmi48
Ack-by: jfehrle
Ack-by: SkySkimmer
|
|
|
|
|
|
Reviewed-by: gares
Reviewed-by: ppedrot
|
|
|
|
to check for conversion
Reviewed-by: gares
Ack-by: SkySkimmer
|
|
Reviewed-by: SkySkimmer
|
|
notation declarations
Reviewed-by: JasonGross
Reviewed-by: Zimmi48
Ack-by: jfehrle
|
|
The table of coercion classes (`class_tab`) has been extended with information
about reachability. The conversion checking of a pair of multiple inheritance
paths (of coercions) will be skipped if these paths can be reduced to smaller
adjoining pairs of multiple inheritance paths, and this reduction will be
determined based on that reachability information.
|
|
Reviewed-by: SkySkimmer
Ack-by: jfehrle
|
|
|
|
The table of coercion classes `class_tab` is now indexed by `cl_typ` instead of
integers (`cl_index`). All the uses of `cl_index` and `Bijint` have been
replaced with `cl_typ` and `ClTypMap` respectively.
|
|
|
|
|
|
|
|
Signed primitive integers defined on top of the existing unsigned ones
with two's complement.
The module Sint63 includes the theory of signed primitive integers that
differs from the unsigned case.
Additions to the kernel:
les (signed <=), lts (signed <), compares (signed compare),
divs (signed division), rems (signed remainder),
asr (arithmetic shift right)
(The s suffix is not used when importing the Sint63 module.)
The printing and parsing of primitive ints was updated and the
int63_syntax_plugin was removed (we use Number Notation instead).
A primitive int is parsed / printed as unsigned or signed depending on
the scope. In the default (Set Printing All) case, it is printed in
hexadecimal.
|
|
|
|
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
|
|
|
