aboutsummaryrefslogtreecommitdiff
path: root/test-suite
AgeCommit message (Collapse)Author
2020-11-13Make the universe of primitive arrays irrelevantGaëtan Gilbert
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.
2020-11-12Merge PR #13359: Print failed test suite logs in CIcoqbot-app[bot]
Reviewed-by: ejgallego Reviewed-by: herbelin
2020-11-12Merge PR #13351: Fixes #13349: accept Search on subparts of an identifier, ↵coqbot-app[bot]
not only on subidentifiers of an identifier Reviewed-by: Zimmi48
2020-11-12Print failed test suite logs in CIGaëtan Gilbert
in addition to having them as artefacts
2020-11-12Add the test as a misc script.Pierre-Marie Pédrot
I left the other test as a v file since it might become relevant when the corresponding Qed bug is fixed.
2020-11-12Fix #13330: Kernel messes with polymorphic side-effects.Pierre-Marie Pédrot
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.
2020-11-12Merge PR #13317: [ssr] intro pattern extensions for dup, swap and applycoqbot-app[bot]
Reviewed-by: gares Ack-by: Zimmi48
2020-11-11Addressing #13349: accept Search on subparts of ident, not only on subidents.Hugo Herbelin
2020-11-10Merge PR #13335: Fix running unit tests with dune compiled coqcoqbot-app[bot]
Reviewed-by: ejgallego
2020-11-10Fix running unit tests with dune compiled coqGaëtan Gilbert
(for runs outside dune, ie "make -C test-suite unit-tests" rather than "dune build @runtest") Fix #13333
2020-11-10Merge PR #13325: [compat] remove 8.10coqbot-app[bot]
Reviewed-by: Zimmi48
2020-11-09[obligation] Proper handle no obligations on `Next Obligation`Emilio Jesus Gallego Arias
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.
2020-11-09[compat] remove 8.10Enrico Tassi
2020-11-09Merge PR #13217: Addresses #13216: use of type classes in the return clause ↵Pierre-Marie Pédrot
of a match. Reviewed-by: ppedrot
2020-11-08fixupCyril Cohen
2020-11-06Merge PR #13255: Fixes #13244: support for coercions in Searchcoqbot-app[bot]
Reviewed-by: SkySkimmer
2020-11-06Merge PR #13284: Fixing interpretation of rewrite_strat argument in LtacPierre-Marie Pédrot
Reviewed-by: ppedrot
2020-11-06Intro pattern extensions for dup, swap and applyCyril Cohen
2020-11-05Regression tests for the various combinations of mixed terms and binders in ↵Hugo Herbelin
notations. This also includes tests for abbreviations.
2020-11-05Fixes #13216 (use of type classes in the return clause of a match).Hugo Herbelin
This was deactivated in fb1c2a017e but it seems useful (e.g. in contribs containers). It seems to be useful
2020-11-05Merge PR #12218: Numeral notations for non inductive typescoqbot-app[bot]
Reviewed-by: herbelin Reviewed-by: JasonGross Reviewed-by: jfehrle Ack-by: Zimmi48
2020-11-05Merge PR #13301: Fixes #13298: Search applied to primitive projections needs ↵coqbot-app[bot]
a correct typing environment Reviewed-by: SkySkimmer
2020-11-05Merge PR #13191: Fix anomaly when importing a functorPierre-Marie Pédrot
Reviewed-by: ppedrot
2020-11-05Merge PR #13182: Check types when converting irrelevant terms in old unificationcoqbot-app[bot]
Reviewed-by: gares
2020-11-05Rename Dec and HexDec to Decimal and HexadecimalPierre Roux
As noted by Hugo Herbelin, Dec is rather used for "decidable".
2020-11-05Allow multiple primitive notation on the same scope and triggersPierre Roux
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.
2020-11-05[string notation] Handle parameterized inductives and non inductivesPierre Roux
2020-11-05[numeral notation] Add support for parameterized inductivesPierre Roux
2020-11-05[numeral notation] Add tests for implicit argumentsPierre Roux
2020-11-05[numeral notation] RPierre Roux
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.
2020-11-05[numeral notation] QPierre Roux
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).
2020-11-04[numeral notation] Add tests for the via ... using ... optionPierre Roux
2020-11-04Typing patterns and using type constraints in Search.Hugo Herbelin
We accept patterns that we failed to type as a fallback.
2020-11-04Fixes #13298: primitive projections needs a correct typing environment.Hugo Herbelin
2020-11-04Merge PR #13302: Fix test-suite in async mode.coqbot-app[bot]
Reviewed-by: SkySkimmer
2020-11-03Merge PR #13132: Understand Mangle Names in implicit generalizationcoqbot-app[bot]
Reviewed-by: herbelin
2020-11-03Merge PR #13179: Fix printing for empty primitive arrayscoqbot-app[bot]
Reviewed-by: herbelin
2020-11-03Merge PR #13256: Remove test-suite/bugs/opened/bug_3395.v: not a bugcoqbot-app[bot]
Reviewed-by: herbelin
2020-11-03Merge PR #13092: Fixing #13078: stack overflow and anomalies with binding ↵coqbot-app[bot]
notations in patterns Reviewed-by: ejgallego Ack-by: ppedrot Ack-by: LasseBlaauwbroek
2020-11-03Fix test-suite in async mode.Théo Zimmermann
(By closing unfinished proofs.)
2020-11-02Nicer spacing when printing array literalsGaëtan Gilbert
From [|x; y; z | def : ty |] to [| x; y; z | def : ty |]
2020-11-02Fix printing for empty primitive arraysGaëtan Gilbert
Fix #13178
2020-11-02Merge PR #13183: attribute #[using] for Definition and Fixpointcoqbot-app[bot]
Reviewed-by: SkySkimmer Ack-by: herbelin Ack-by: Zimmi48
2020-11-02Merge PR #13274: Fix two bugs in conversion of primitive valuescoqbot-app[bot]
Reviewed-by: SkySkimmer
2020-11-02Merge PR #13247: Fixes #13241: nested Ltac functions wrongly reporting error ↵Pierre-Marie Pédrot
on the inner calls Reviewed-by: ppedrot
2020-11-02[stm] support #[using] attributeEnrico Tassi
2020-11-02attribute #[using] for Definition and FixpointEnrico Tassi
2020-10-30Renaming Numeral.v into Number.vPierre Roux
2020-10-29Fixing interpretation of rewrite_strat argument in Ltac.Hugo Herbelin
Ltac variables were not yet supported.
2020-10-29Use same code for "Print Ltac foo" and "Print foo" when "foo" is an Ltac.Hugo Herbelin
Adopting the same format means printing "Ltac foo := ..." and not the fully qualified name of foo.
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-23 21:19:53 +0000