| Age | Commit message (Collapse) | Author |
|---|
|
|
|
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
|
|
|
|
Fixes #13266 (see #12675, 8641cb7385).
|
|
not only on subidentifiers of an identifier
Reviewed-by: Zimmi48
|
|
|
|
Fixes #13320 .
Trivial programming error, actually this is handled better in a
further refactoring branch not submitted due to the long time the
whole rework took.
|
|
Reviewed-by: SkySkimmer
|
|
notations.
This also includes tests for abbreviations.
|
|
Reviewed-by: herbelin
Reviewed-by: JasonGross
Reviewed-by: jfehrle
Ack-by: Zimmi48
|
|
As noted by Hugo Herbelin, Dec is rather used for "decidable".
|
|
Until now, declaring a number or string notation on some trigger
removed all previous notations on the same scope.
Bug discovered by Jason Gross while reviewing #12218.
|
|
|
|
|
|
|
|
Previously real constants were parsed by an unproved OCaml code. The
parser and printer are now implemented in Coq, which will enable a
proof and hopefully make it easier to maintain / make evolve.
Previously reals were all parsed as an integer, an integer multiplied
by a power of ten or an integer divided by a power of ten. This means
1.02 and 102e-2 were both parsed as 102 / 100 and could not be tell
apart when printing. So the printer had to choose between two
representations : without exponent or without decimal dot. The choice
was made heuristically toward a most compact representation.
Now, decimal dot is parsed as a rational and exponents are parsed as a
product or division by a power of ten. For instance, 1.02 is parsed as
Q2R (102 # 100) whereas 102e-2 is parsed as IZR 102 / IZR (Z.pow_pos
10 2).
1.02 and 102e-2 remain equal (proved by reflexivity) but 1.02e1 = Q2R
(102 # 100) * 10 and 10.2 = Q2R (102 # 10) no longer are.
|
|
Previously rationals were all parsed as a pair numerator, denominator.
This means 1.02 and 102e-2 were both parsed as 102 # 100 and could not
be tell apart when printing. So the printer had to choose between two
representations : without exponent or without decimal dot. The choice
was made heuristically toward a most compact representation.
Now, decimal dot is still parsed as a power of ten denominator but
exponents are parsed as a product or division by Z.pow_pos. For
instance, 1.02 is parsed as 102 # 100 whereas 102e-2 is parsed as
(102 # 1) / (Z.pow_pos 10 2 # 1).
1.02 and 102e-2 remain equal (proved by reflexivity) but 1.02e1
= (102 # 100) * (10 # 1) = 1020 # 100 and 10.2 = 102 # 10 no longer are.
A nice side effect is that exponents can no longer blow up during
parsing. Previously 1e1_000_000 literally produced a numerator with a
million digits, now it just yields (1 # 1) * (Z.pow_pos 10 1_000_000 # 1).
|
|
|
|
We accept patterns that we failed to type as a fallback.
|
|
|
|
Reviewed-by: SkySkimmer
|
|
(By closing unfinished proofs.)
|
|
From
[|x; y; z | def : ty |]
to
[| x; y; z | def : ty |]
|
|
on the inner calls
Reviewed-by: ppedrot
|
|
|
|
Adopting the same format means printing "Ltac foo := ..." and not the
fully qualified name of foo.
|
|
inner calls).
This continues #12223, #12773, #12992, #12774, #12999.
|
|
Reviewed-by: gares
Reviewed-by: herbelin
Ack-by: ppedrot
|
|
|
|
pattern-matching clause with unused named variable
Reviewed-by: jfehrle
Reviewed-by: vbgl
Ack-by: gares
|
|
|
|
Similar to `dependent induction`, report an error message for `dependent
destruction` saying that importing `Coq.Program.Equality` is required,
rather than failing at parsing time.
This is a small extension of #605 to cover dependent destruction as
well. Here I also put in some tests.
|
|
Reviewed-by: ejgallego
Reviewed-by: Zimmi48
|
