aboutsummaryrefslogtreecommitdiff
path: root/test-suite/bugs/closed
AgeCommit message (Collapse)Author
2020-03-26Fix #11845: anomaly when including partially applied functorGaëtan Gilbert
2020-03-23Fix levels of `<=?` and `<?` in the stdlibJason Gross
They were defined at level 70, no associativity in all but three places, where they were instead declared at level 35. Fixes #11890
2020-03-17Properly thread let-bindings in Funind principle construction.Pierre-Marie Pédrot
Fixes #11846: Funind fails to generate principles for terms with let bindings.
2020-03-17Merge PR #11811: Remove a positivity check when Positivity Checking is offGaëtan Gilbert
Reviewed-by: SkySkimmer
2020-03-17Add test for PR11811 (disable a positivity check)SimonBoulier
2020-03-13Implementing postponed constraints in TC resolutionMatthieu Sozeau
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
2020-03-11Merge PR #11769: Fix #9930: "change" replaces 0-param projections by constantsPierre-Marie Pédrot
Reviewed-by: ppedrot
2020-03-09Fix #11730: Mangle Names vs InfixGaëtan Gilbert
2020-03-09Fix #9930: "change" replaces 0-param projections by constantsGaëtan Gilbert
2020-03-06Merge PR #11723: Fix mishandling of sigma in guess_elim (regression from 8.11)Pierre-Marie Pédrot
Reviewed-by: ppedrot
2020-03-01test-suite file for spurious universe generationMatthieu Sozeau
2020-02-28Merge PR #11609: [stm] Use Default Proof Using only with ProofEnrico Tassi
2020-02-28[stm] Use Default Proof Using only with ProofTej Chajed
Fixes #11608. This means -vos doesn't skip proofs for definitions that end with Qed but don't include Proof and rely on a Set Default Proof Using. However, this fixes the bug where this pattern would instead hang, due to #11564.
2020-02-26Consolidate int63-related notationsMaxime Dénès
We avoid redundant notations for the same concepts and make sure notations do not break Ltac parsing for users of these libraries.
2020-02-24Merge PR #11560: Fix #11549: Ltac2 is incompatible with $.Tej Chajed
Reviewed-by: tchajed
2020-02-23Merge pull request #11629 from ppedrot/fix-11552Tej Chajed
Fix #11552: Ltac2 breaks query commands during proofs.
2020-02-22Merge PR #11639: Fixes #10917: anomaly in building return clause of n-ary ↵Emilio Jesus Gallego Arias
pattern-matching problem Reviewed-by: ejgallego
2020-02-21Notations: Avoiding computing parsing rule when in onlyprinting mode.Hugo Herbelin
In particular, this fixes #9741.
2020-02-20Fixing #11114 (anomaly with Extraction Implicit on records).Hugo Herbelin
This was due to an inconsistency in handling implicit arguments in the fields and in the constructor of a record.
2020-02-20Fixes #10917 (missing lift in building return clause by inversion).Hugo Herbelin
2020-02-19Fix #11549: Ltac2 is incompatible with $.Pierre-Marie Pédrot
We use the same kind of trick as the one we used for &IDENT, namely check that no space appear between the dollar sign and the identifier.
2020-02-19Fix #11552: Ltac2 breaks query commands during proofs.Pierre-Marie Pédrot
Actually, callers of the Pvernac.register_proof_mode function have to manually register the parsing of vernacular queries themselves. This probably qualifies as an oversight from myself.
2020-02-16Fixing bug #9521 (anomaly due to missing declaration of level in custom entry).Hugo Herbelin
This fixes also #9640 part 1.
2020-02-15Fixes #11331 (unexpected level collisions between custom entries and constr).Hugo Herbelin
There was a collision at the time of interpreting subentries (in metasyntax.ml) but also at the time of "optimizing" the entries (in egramcoq.ml). Also fixes #9517, fixes #9519, fixes #9640 (part 3).
2020-02-11Merge PR #11554: Fix #11553: magicaly_constant_of_fixbody checks existence ↵Pierre-Marie Pédrot
of made up constant Reviewed-by: ppedrot
2020-02-09Merge PR #11518: Fix #11515: Ltac2 rewrite on wildcard.Gaëtan Gilbert
Reviewed-by: SkySkimmer
2020-02-09Fix #11553: magicaly_constant_of_fixbody checks existence of made up constantGaëtan Gilbert
2020-02-04Fix #11515: Ltac2 rewrite on wildcard.Pierre-Marie Pédrot
There was an evar leak due to an evarmap not being threaded correctly when computing open terms.
2020-02-03Test for #5617: Primitive projections confuse the termination checker.Pierre-Marie Pédrot
Fixes #5617.
2020-01-22Fix #11421 computation of Set+2Gaëtan Gilbert
2020-01-19Merge PR #11368: Turn trailing implicit warning into an errorHugo Herbelin
Ack-by: Zimmi48 Reviewed-by: herbelin Ack-by: maximedenes
2020-01-15Merge PR #11373: Close #11168Pierre-Marie Pédrot
Reviewed-by: ppedrot
2020-01-08Close #11133Gaëtan Gilbert
Fixed by 8750682e367d7e78634bf88e667e4c9e7c3613d3 (#9915)
2020-01-08Close #11168Gaëtan Gilbert
Seems to have been fixed since it was reported (perhaps by #11317?)
2020-01-07Fix test-suite fo non maximal implicit argumentsSimonBoulier
2020-01-06Fix #11360: discharge of template inductive with param only use of varGaëtan Gilbert
2019-12-27Add critical-bugs entry, tests-suite file, and code comment.Guillaume Melquiond
2019-12-14Fix refine and eapply to mark shelved goals as non-resolvable, alwaysMatthieu Sozeau
Check that we don't regress on PR #10762 example Fix regression discovered by Arthur in PR #10762 Fix script of #10298 which was relying on breaking semantics for `eapply` Add doc Add comment in clenvtac Actually, always mark shelved goals as unresolvable Update doc to reflect semantics w.r.t. shelved subgoals
2019-11-29Merge PR #11076: Remove all remaining calls to “omega” from the standard ↵Emilio Jesus Gallego Arias
library Reviewed-by: ejgallego
2019-11-27Merge PR #11128: Fix #11039: proof of False with template poly and nonlinear ↵Pierre-Marie Pédrot
universes Reviewed-by: Zimmi48 Reviewed-by: mattam82 Reviewed-by: ppedrot
2019-11-26Fix #11039: proof of False with template poly and nonlinear universesGaëtan Gilbert
Using the parameter universes in the constructor causes implicit equality constraints, so those universes may not be template polymorphic. A couple types in the stdlib were erroneously marked template, which is now detected. Removing the marking doesn't actually change behaviour though. Also fixes #10504.
2019-11-25Test-suite: avoid using “omega”Vincent Laporte
2019-11-22Add test for #11161Gaëtan Gilbert
This is better than expecting other tests to fail if we mess up again.
2019-11-19Fixing bugs in the computation of implicit arguments for fix with a let binder.Hugo Herbelin
2019-11-12Merge PR #11045: Forbid Include inside sectionsPierre-Marie Pédrot
Ack-by: Blaisorblade Reviewed-by: gares Reviewed-by: ppedrot
2019-11-11Merge PR #11052: Fix #11048: uncaught destKO in inductive typePierre-Marie Pédrot
Reviewed-by: ppedrot
2019-11-10Merge PR #10980: Fix #10903: type-in-type allows fixpoints on sprop inductivesPierre-Marie Pédrot
Reviewed-by: ppedrot
2019-11-08Merge PR #11014: Fix #8459: anomaly not enough abstractions in fix bodyPierre-Marie Pédrot
Reviewed-by: ppedrot
2019-11-07Merge PR #11049: Prevent redefinition of Ltac2 types and constructors inside ↵Pierre-Marie Pédrot
a module Reviewed-by: ppedrot
2019-11-06Swap parsing precedence of `::` and `,` ; Fix #10116Kenji Maillard
generated by cgit v1.2.3 (git 2.25.1) at 2026-06-29 16:52:42 +0000