| Age | Commit message (Collapse) | Author |
|---|
|
handler in NotFoundInstance
Reviewed-by: ejgallego
|
|
|
|
|
|
Fix #6042
Also introduce a deprecated compat option
|
|
This allows the following to interpret "0" in the expected scope:
Notation "0" := true : bool_scope.
Axiom f : bool -> bool -> nat.
Record R := { p : bool -> nat }.
Check (@f 0) 0.
Check fun r => r.(@p) 0.
|
|
a keyword.
Ack-by: SkySkimmer
Reviewed-by: herbelin
Ack-by: ppedrot
|
|
Reviewed-by: ppedrot
|
|
This does not affect the rendering but gives better structured
html/tex files.
|
|
We clarify that there are two kinds of verbatim: inline and block.
We add a test testing verbatim and others.
Co-authored-by: Xia Li-yao <Lysxia@users.noreply.github.com>
|
|
Fixes #13266 (see #12675, 8641cb7385).
|
|
In Evar := C[Meta] problems of unification.ml, and C[ ] contains
binders, Meta was wrongly considered by pose_all_metas_as_evars as
under these binders (while Metas are always defined in the initial
context of the unification problem).
|
|
Fix #13348
|
|
Fix #13354
This change is very specific to array, but should not be a significant
obstacle to generalization of the feature to eg axioms if we want to later.
|
|
|
|
Reviewed-by: ejgallego
Reviewed-by: herbelin
|
|
not only on subidentifiers of an identifier
Reviewed-by: Zimmi48
|
|
in addition to having them as artefacts
|
|
I left the other test as a v file since it might become relevant when the
corresponding Qed bug is fixed.
|
|
Polymorphic side-effects generated in monomorphic mode would be counted towards
trusted subcomponents. This would allow to make ill-typed terms pass as
legitimate by mimicking the shape of the inlining of monomorphic side-effects in
such a proof.
|
|
Reviewed-by: gares
Ack-by: Zimmi48
|
|
|
|
Reviewed-by: ejgallego
|
|
(for runs outside dune, ie "make -C test-suite unit-tests" rather than
"dune build @runtest")
Fix #13333
|
|
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.
|
|
|
|
of a match.
Reviewed-by: ppedrot
|
|
|
|
Reviewed-by: SkySkimmer
|
|
Reviewed-by: ppedrot
|
|
|
|
notations.
This also includes tests for abbreviations.
|
|
This was deactivated in fb1c2a017e but it seems useful (e.g. in
contribs containers).
It seems to be useful
|
|
Reviewed-by: herbelin
Reviewed-by: JasonGross
Reviewed-by: jfehrle
Ack-by: Zimmi48
|
|
a correct typing environment
Reviewed-by: SkySkimmer
|
|
Reviewed-by: ppedrot
|
|
Reviewed-by: gares
|
|
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
|
|
Reviewed-by: herbelin
|
|
Reviewed-by: herbelin
|
