aboutsummaryrefslogtreecommitdiff
path: root/test-suite/bugs
AgeCommit message (Collapse)Author
2020-11-15Default disable automatic generalization of Instance typeGaëtan Gilbert
Fix #6042 Also introduce a deprecated compat option
2020-11-15Merge PR #13350: Fix incorrect "avoid" set in globenv extra dataPierre-Marie Pédrot
Reviewed-by: ppedrot
2020-11-13Fix incorrect "avoid" set in globenv extra dataGaëtan Gilbert
Fix #13348
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-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-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-06Merge PR #13284: Fixing interpretation of rewrite_strat argument in LtacPierre-Marie Pédrot
Reviewed-by: ppedrot
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 #13191: Fix anomaly when importing a functorPierre-Marie Pédrot
Reviewed-by: ppedrot
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-02Fix printing for empty primitive arraysGaëtan Gilbert
Fix #13178
2020-10-29Fixing interpretation of rewrite_strat argument in Ltac.Hugo Herbelin
Ltac variables were not yet supported.
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-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 #12955: Reroot primitive arrays on accesscoqbot-app[bot]
Reviewed-by: maximedenes
2020-10-19Addressing parsing part #13078.Hugo Herbelin
We don't give sense to pattern/binders in leftmost position.
2020-10-19Fixing printing part of #13078 (anomaly with binding notations in patterns).Hugo Herbelin
We prevent notations involving binders (i.e. names or patterns) to be used for printing in "match" patterns. The computation is done in "has_no_binders_type", controlling uninterpretation.
2020-10-19Merge PR #13192: Fix algebraic on the right when using bidi hintscoqbot-app[bot]
Reviewed-by: gares
2020-10-15Merge PR #12925: [declare] Fix types of mutual lemmas when using Admitted.coqbot-app[bot]
Reviewed-by: herbelin Ack-by: SkySkimmer
2020-10-15Merge PR #13181: Guard unify_leq_delay calls in TypingPierre-Marie Pédrot
Reviewed-by: ppedrot
2020-10-15[declare] Fix types of mutual lemmas when using Admitted.Emilio Jesus Gallego Arias
We fix a clear coding mistake in 79bcf1c0a22e736c4e2cae3460c35b3d9fca9aa0 that forgot to update the type of the parameter entry when saving mutual definitions without a body. We follow the solution suggested by Hugo Herbelin and drop the type used in `start_proof`. Note the duplication here indeed. Fixes #12895 Co-authored-by: Hugo Herbelin <Hugo.Herbelin@inria.fr>
2020-10-14Fix algebraic on the right when using bidi hintsGaëtan Gilbert
Fix #12970 We can't recover the expected type of the post bidi argument by retyping because the hole may be filled by something in which case retyping can produce algebraic universes.
2020-10-14Fix anomaly when importing a functorGaëtan Gilbert
Fix #13162
2020-10-13Merge PR #13172: Fix #13169: vm_compute has existential crisis.coqbot-app[bot]
Reviewed-by: silene
2020-10-12Guard unify_leq_delay calls in TypingGaëtan Gilbert
Fix #13171
2020-10-11Fix #13169: vm_compute has existential crisis.Pierre-Marie Pédrot
We simply use evars instance in the right order while reading back VM values.
2020-10-09No bidirectionality when expected type for lambda is an evar.Gaëtan Gilbert
This fixes #12623 (bidirectionality breaks impredicativity).
2020-10-09Minimize Prop <= i to i := SetGaëtan Gilbert
Fix part of #8196, fix #12414 Replaces #9343
2020-10-09Merge PR #13087: Put type-in-type flag in ugraph.Pierre-Marie Pédrot
Reviewed-by: ppedrot
2020-10-08Check complexity of primitive arrays.Guillaume Melquiond
2020-10-07Merge PR #13115: Derive Inversion does not allow leftover evarsPierre-Marie Pédrot
Reviewed-by: ppedrot
2020-10-06Implicit_quantifiers don't use precomputed is_class dataGaëtan Gilbert
Fix #13117 We alternatively could fix the generation of the data with Existing Class but I prefer moving towards removing it.
2020-10-02setoid_rewrite: record generated name when rewriting under lambdaGaëtan Gilbert
Fix #13129
2020-10-02Understand Mangle Names in implicit generalizationGaëtan Gilbert
Fix #13131
2020-10-02Merge PR #13106: Remove the forward class hint feature.coqbot-app[bot]
Reviewed-by: SkySkimmer
2020-10-01Merge PR #13114: Reimplement Admit Obligations using standard Admitted codecoqbot-app[bot]
Reviewed-by: ejgallego
2020-09-30Fix combining uniform parameters and mutual inductives.Jasper Hugunin
2020-09-30Remove the forward class hint feature.Pierre-Marie Pédrot
It was not documented, not properly tested and thus likely buggy. Judging from the code alone I spotted already one potential bug. Further more it was prominently making use of the infamous "arbitrary term as hint" feature. Since the only user in our CI seems to be a math-classes file that introduced the feature under a claim of "cleanup", I believe we can safely remove it without anyone noticing.
2020-09-30Derive Inversion does not allow leftover evarsGaëtan Gilbert
Fix #12917
2020-09-30Reimplement Admit Obligations using standard Admitted codeGaëtan Gilbert
Fix #13109
2020-09-28Put type-in-type flag in ugraph.Gaëtan Gilbert
Fix #13086.
2020-09-10Use fresher names in eqschemes.Jasper Hugunin
The previous implementation appears to be sound when Mangle Names is off, but it relies on two fragile assumptions, namely that next_global_ident_away always returns different identifiers when called with naming hints which are different after stripping all digits from the end, and that default_id_of_sort (locally defined) never returns "HC" or "P", or either of those followed by a string of digits. These changes make both assumptions unnecessary. As a side note, it seems odd that fresh is ignoring it's env parameter.
2020-09-09Merge PR #7825: [tactics] Refine test for unresolved evars: not reachable ↵Pierre-Marie Pédrot
from initial evars Ack-by: JasonGross Ack-by: Zimmi48 Reviewed-by: ejgallego Reviewed-by: gares Ack-by: jfehrle Ack-by: maximedenes Reviewed-by: ppedrot
2020-09-08Merge PR #12931: Proof using cleanup, small doc addition and fix using Type ↵coqbot-app[bot]
in collections Reviewed-by: gares Ack-by: Zimmi48
2020-09-08Merge PR #12954: Fixes a freshness issue with destruct/induction (see ↵Pierre-Marie Pédrot
comment in #12944). Ack-by: RalfJung Ack-by: jashug Reviewed-by: ppedrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-10-13 15:43:28 +0000