aboutsummaryrefslogtreecommitdiff
path: root/test-suite
AgeCommit message (Collapse)Author
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-31Closes #13278: take into account elimination constraints in small inversion.Hugo Herbelin
Ideally, if equations t <= ?x were preserving subtyping that could be simpler. Currently we need however to put a rigid universe as constraint on the return predicate so that one branch does not force the return sort to be lower by unification than what another branch would have needed.
2020-10-31Fine-tuning the sort of the predicate obtained by small inversion.Hugo Herbelin
If the result is in SProp, Prop or (impredicative) Set, we preserve this information since the elimination sort might be restricted by the sort of the destructed type. If the result is in Type, we use a fresh sort upper bound so that we are sure not having residual algebraic universes which would raise problems in a type constraint (e.g. in define_evar_as_product). This fixes the part of #13278 posted on discourse.
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.
2020-10-28Fixes #13241 (nested Ltac functions were wrongly reporting error on the ↵Hugo Herbelin
inner calls). This continues #12223, #12773, #12992, #12774, #12999.
2020-10-27Merge PR #13238: Fix some tactic print bugscoqbot-app[bot]
Reviewed-by: gares Reviewed-by: herbelin Ack-by: ppedrot
2020-10-27Rename operconstr -> termJim Fehrle
2020-10-26Merge PR #12768: Granting wish #12762: warning on duplicated catch-all ↵coqbot-app[bot]
pattern-matching clause with unused named variable Reviewed-by: jfehrle Reviewed-by: vbgl Ack-by: gares
2020-10-26Adding a test for the second bug.Pierre-Marie Pédrot
2020-10-22Remove test-suite/bugs/opened/bug_3395.v: not a bugGaëtan Gilbert
2020-10-22Fix printing of wit_constr and some ssr problems with printing empty listsLasse Blaauwbroek
2020-10-22Merge PR #13130: setoid_rewrite: record generated name when rewriting under ↵Pierre-Marie Pédrot
lambda Reviewed-by: ppedrot
2020-10-21Merge PR #13118: [type classes] Simplify cl_contextPierre-Marie Pédrot
Reviewed-by: ppedrot
2020-10-21Merge PR #13201: Report a useful error for dependent destructionPierre-Marie Pédrot
Reviewed-by: ppedrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-02 02:32:39 +0000