| Age | Commit message (Collapse) | Author |
|---|
|
The location was missing in the parser.
|
|
In particular, the error messages do not mention anymore the notion of
bool-valued options, since these are documented as flags and work
quite differently from the rest of options.
|
|
It seems that this PR is making the rewrite much, much faster.
|
|
|
|
Reviewed-by: ejgallego
Reviewed-by: ppedrot
|
|
Reviewed-by: ejgallego
|
|
|
|
Co-authored-by: Jasper Hugunin <jasper@hugunin.net>
Co-authored-by: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
|
|
Reviewed-by: ppedrot
|
|
grammar.
Reviewed-by: ejgallego
Reviewed-by: maximedenes
|
|
Ack-by: SkySkimmer
Reviewed-by: Zimmi48
Reviewed-by: erikmd
|
|
|
|
|
|
We clean the hack bypassing the interpretation of "'pat" in binders
and move it to comDefinition.ml. In particular, we fix the exact
subterm to which Eval has to apply in the hack, and remove the
artificial cast we had introduced.
|
|
Reviewed-by: herbelin
|
|
|
|
|
|
Reviewed-by: herbelin
|
|
For instance, parsing 0.1 will print a warning whereas parsing 0.5 won't.
|
|
Print 1.5 as 1.5 and not 15e-1.
We choose the shortest representation
with tie break to the dot notation (0.01 rather than 1e-3).
The printing remains injective, i.e. 12/10 is not mixed with 120/100,
the first being printed as 1.2 and the last as 1.20.
|
|
Print 1.5 as 1.5 and not 15e-1.
We choose the shortest representation
with tie break to the dot notation (0.01 rather than 1e-3).
The printing remains injective, i.e. 12*10^2 is printed 12e2 in order
not to mix it with 1200 and 12/10^1 is not mixed with 120/10^2, the
first being printed as 1.2 and the last as 1.20.
|
|
They were defined at level 70, no associativity in all but three places,
where they were instead declared at level 35.
Fixes #11890
|
|
|
|
Originally from bedrock2.
|
|
|
|
Four types of numerals are introduced:
- positive natural numbers (may include "_", e.g. to separate thousands, and leading 0)
- integer numbers (may start with a minus sign)
- positive numbers with mantisse and signed exponent
- signed numbers with mantisse and signed exponent
In passing, we clarify that the lexer parses only positive numerals,
but the numeral interpreters may accept signed numerals.
Several improvements and fixes come from Pierre Roux. See
https://github.com/coq/coq/pull/11703 for details. Thanks to him.
|
|
Ack-by: SkySkimmer
Reviewed-by: jfehrle
Reviewed-by: ppedrot
|
|
Ack-by: SkySkimmer
Ack-by: Zimmi48
Reviewed-by: gares
|
|
Reviewed-by: Matafou
|
|
Unfortunately, we cannot go further and parse Export as a legacy
attribute because this syntax conflicts with the Export command.
|
|
Reviewed-by: JasonGross
Reviewed-by: Zimmi48
|
|
|
|
Ack-by: herbelin
|
|
Reviewed-by: JasonGross
Reviewed-by: ppedrot
|
|
|
|
|
|
That is, it contains the type of the binder so as not to rely on the relevance
explicitly.
|
|
Reviewed-by: jfehrle
|
|
Add headers to a few files which were missing them.
|
|
|
|
|
|
Fixes #11846: Funind fails to generate principles for terms with let bindings.
|
|
Reviewed-by: SkySkimmer
|
|
|
|
|
|
This was accidentaly disabled by #6264 when no_native_compiler was
renamed to native_compiler.
Moreover, the (then unactivated test) was broken by commit 48ae6ce
(part of #9088).
|
|
|
|
Reviewed-by: SkySkimmer
Ack-by: Zimmi48
Ack-by: ejgallego
|
|
A constraint can be stuck if it does not match any of the declared modes
for its head (if there are any). In that case, the subgoal is postponed
and the next ones are tried. We do a fixed point computation until there
are no stuck subgoals or the set does not change (it is impossible to
make it grow, as asserted in the code, because it is always a subset of
the initial goals)
This allows constraints on classes with modes to be treated as if they were
in any order (yay for stability of solutions!). Also, ultimately it should
free us to launch resolutions more agressively (avoiding issues like the
ones seen in PR #10762).
Add more examples of the semantics of TC resolution with apply in test-suite
Properly catch ModeMatchFailure on calls to map_e*
Add fixed bug 9058 to the test-suite
Close #9058
Add documentation
Fixes after Gaëtan's review.
Main change is to not use exceptions for control-flow
Update tactics/class_tactics.ml
Clearer and more efficient mode mismatch dispatch
Co-Authored-By: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
Remove exninfo argument
|
|
Ack-by: SkySkimmer
Reviewed-by: gares
|
