| Age | Commit message (Collapse) | Author |
|---|
|
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).
|
|
Just to get a cleaner log, this will be proved again in a few commits.
|
|
|
|
|
|
This enables numeral notations for non inductive types by
pre/postprocessing them to a given proxy inductive type.
For instance, this should enable the use of numeral notations for R.
|
|
This will enable to define numeral notation on non inductive by using
an inductive type as proxy and those translations to translate to/from
the actual type to the inductive type.
|
|
|
|
This is a generated file since #13147
|
|
|
|
|
|
|
|
Reviewed-by: gares
Reviewed-by: herbelin
Ack-by: ppedrot
|
|
grammars more consistent
Reviewed-by: Zimmi48
Reviewed-by: herbelin
Ack-by: SkySkimmer
|
|
Reviewed-by: gares
|
|
|
|
typ_param -> ltac2_typevar,
tac2expr -> ltac2_expr
|
|
|
|
|
|
|
|
Reviewed-by: SkySkimmer
Ack-by: gares
Ack-by: ejgallego
|
|
Reviewed-by: ejgallego
Reviewed-by: gares
Reviewed-by: ppedrot
|
|
Reviewed-by: vbgl
|
|
pattern-matching clause with unused named variable
Reviewed-by: jfehrle
Reviewed-by: vbgl
Ack-by: gares
|
|
|
|
Using it feels nicer this way, with GADT details hidden inside comtactic
|
|
Reviewed-by: Zimmi48
Reviewed-by: Blaisorblade
|
|
functions
Reviewed-by: SkySkimmer
|
|
|
|
Reviewed-by: herbelin
|
|
Reviewed-by: Zimmi48
Ack-by: mattam82
Ack-by: pi8027
Ack-by: herbelin
Ack-by: gares
Ack-by: fajb
Ack-by: proux01
|
|
|
|
Reviewed-by: Zimmi48
Reviewed-by: jfehrle
|
|
The cast keywords are <: and <<:, not :>/:>>
:>> stopped being a keyword in #13106
|
|
Reviewed-by: Zimmi48
|
|
We move quite a few obligation functions from a `let rec ... and`
block, as they are not mutually recursive.
By the way, we perform some refactoring on `solve_by_tac`, which is
quite messy still, but now the code flow could actually accommodate
passing a declaration entry instead of low-level objects.
[It seems that we will need to introduce a special obligation entry
for that purpose, but thankfully it will be internal. We are actually
pretty close on being able to remove `build_by_tactic`, which we
should do ASAP due to its current semantics breaking abstraction
barriers]
|
|
Git wants an identity and none is setup on the CI.
|
|
Fixup #13050.
|
|
Reviewed-by: Zimmi48
|
|
Always generate prodn* files if edits succeed
|
|
Reviewed-by: jfehrle
|
|
|
|
Reviewed-by: ppedrot
|
|
Reviewed-by: vbgl
|
|
This allows native_compute to work and is the same fix that was
applied to the nixpkgs repo in NixOS/nixpkgs#101058.
|
|
lambda
Reviewed-by: ppedrot
|
|
|
|
Reviewed-by: herbelin
Ack-by: SkySkimmer
|
|
|
|
This fixes a regression introduced in #11618, where I didn't realize
that the order of ML includes would be important as users may want to
shadow it.
In general I do believe that shadowing is tricky and the build system
should handle it, but for now makes sense to preserver the behavior.
The fix is not very nice, but we cannot afford to tweak the API as
this should be backported to 8.12.1; there is a pending PR refactoring
a bit more the toplevel init that should clean this up.
Fixes #12771
|
|
Reviewed-by: ppedrot
|
