aboutsummaryrefslogtreecommitdiff
path: root/test-suite/bugs
AgeCommit message (Collapse)Author
2020-05-15Merge PR #11992: do not re-export ListNotations from ProgramAnton Trunov
Reviewed-by: Zimmi48 Reviewed-by: anton-trunov Reviewed-by: ejgallego
2020-05-14Merge PR #12256: Move the static check of evaluability in unfold tactic to ↵Hugo Herbelin
runtime. Reviewed-by: herbelin
2020-05-14Add test for #11727, which was indirectly fixed by this PR.Pierre-Marie Pédrot
2020-05-14Move the static check of evaluability in unfold tactic to runtime.Pierre-Marie Pédrot
See #11840 for a motivation. I had to fix Floats.FloatLemmas because it uses the same name for a notation and a term, and the fact this unfold was working on this was clearly a bug. I hope nobody relies on this kind of stuff in the wild. Fixes #5764: "Cannot coerce ..." should be a runtime error. Fixes #5159: "Cannot coerce ..." should not be an error. Fixes #4925: unfold gives error on Admitted.
2020-05-14Fixes #12234 (wrong environment for Show Proof).Hugo Herbelin
We take the env of the current goal with the context replaced with section variables. In practice, this is the global env, but, maybe, one day, a goal state will have its own env.
2020-05-14Merge PR #8808: Extending support for mixing binders and terms in abbreviationsEmilio Jesus Gallego Arias
Ack-by: Zimmi48 Reviewed-by: ejgallego Reviewed-by: mattam82
2020-05-13Extending support for mixing binders and terms in abbreviations.Hugo Herbelin
2020-05-13Tests for bugs #9583 (fixed by #11613) and #9679.Hugo Herbelin
2020-05-12Merge PR #12146: Fixes #10812: tactic subst failure with section variables ↵Pierre-Marie Pédrot
indirectly dependent in goal Ack-by: Zimmi48 Reviewed-by: ppedrot
2020-05-07Tactic subst now inactive on section variables occurring indirectly in goal.Hugo Herbelin
This is saner behavior making subst reversible, as discussed in #12139. This also fixes #10812 and #12139. In passing, we also simplify a bit the code of "subst_all".
2020-05-06HaskellExtr: Add type annotations to Prelude.==Jason Gross
Also `Export ExtrHaskellBasic` in `ExtrHaskellString`. Fixes #12257 Fixes #12258
2020-05-02LtacProf now handles multi-success backtrackingJason Gross
Fixes #12196
2020-04-30do not re-export ListNotations from Program: fix testsuiteAntonio Nikishaev
2020-04-24Make the nsatz test-suite passJason Gross
2020-04-24Split off Nsatz tactic part into NsatzTacticJason Gross
Closes #5445 Note that we use `Include` rather than `Export` to expose the machinery defined in `NsatzTactic` from `Nsatz` to preserve backwards compatibility with developments relying on absolute names of the constants previously defined in `Nsatz.v`.
2020-04-21Adapt test-suite to #12023.Hugo Herbelin
2020-04-21Merge PR #12116: Fixing #12045: missing normalization in conclusion of ↵Pierre-Marie Pédrot
custom induction scheme Reviewed-by: ppedrot
2020-04-21Merge PR #11883: Fix #7812: autounfold's behavior depends on file namesHugo Herbelin
Reviewed-by: herbelin
2020-04-20Fixing #12045 (missing normalization in conclusion of custom induction scheme).Hugo Herbelin
2020-04-17ZArith: move lia hints to a dedicated moduleVincent Laporte
2020-04-17Merge PR #11972: Fix require in sectionPierre-Marie Pédrot
Ack-by: Zimmi48 Reviewed-by: ppedrot
2020-04-13Close #11935: section variables do not have universe instances.Gaëtan Gilbert
2020-04-13Fix #11783 Require in SectionGaëtan Gilbert
2020-04-11Fix #7812Attila Gáspár
2020-04-03Fix the test for bug #4544.Pierre-Marie Pédrot
It seems that this PR is making the rewrite much, much faster.
2020-04-01Merge PR #11945: Fix #11941: anomaly in equality schemesEmilio Jesus Gallego Arias
Reviewed-by: ejgallego Reviewed-by: ppedrot
2020-03-31Remove special case for implicit inductive parametersMaxime Dénès
Co-authored-by: Jasper Hugunin <jasper@hugunin.net> Co-authored-by: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
2020-03-28Remove SearchAbout command, deprecated in 8.5Jim Fehrle
2020-03-28Fix #11941: anomaly in equality schemesGaëtan Gilbert
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 PR #11120: Refactoring code for application printing + fixing #11091 ↵Emilio Jesus Gallego Arias
(inconsistencies in parsing/printing notations to partial applications) Ack-by: Zimmi48 Reviewed-by: ejgallego Ack-by: jfehrle
2020-02-23Merge pull request #11629 from ppedrot/fix-11552Tej Chajed
Fix #11552: Ltac2 breaks query commands during proofs.
2020-02-22Fixes #4690: do not allow @f in notations when f is a notation variable.Hugo Herbelin
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.
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-25 21:43:49 +0000