aboutsummaryrefslogtreecommitdiff
path: root/test-suite/bugs
AgeCommit message (Collapse)Author
2020-07-09Recordops: unify struc_typ summary record and libobject entry struc_tupleGaëtan Gilbert
This requires updating the parameter count at section end, I felt it was easier to do with rebuild_function but it could be done in discharge if needed. Incidentally fixes #12649.
2020-07-08Merge PR #12627: Fix Canonical with universe polymorphism and primitive ↵Enrico Tassi
projection Reviewed-by: ejgallego Ack-by: gares
2020-07-08Merge PR #12652: Fix erroneous implicits-in-term warningEmilio Jesus Gallego Arias
Reviewed-by: ejgallego Reviewed-by: herbelin
2020-07-07Merge PR #12626: Fix Context with nonmaximplicit.Emilio Jesus Gallego Arias
Reviewed-by: ejgallego
2020-07-07Fix erroneous implicits-in-term warningGaëtan Gilbert
Fix #12651
2020-07-05Fix Canonical with universe polymorphism and primitive projectionGaëtan Gilbert
Perhaps we should thread an evar map with the Var universes added through to cs_pattern_of_constr but that would be significantly more invasive. Fix #12528
2020-07-03Fix #11121: Simultaneous definition of term and notation in custom grammarMaxime Dénès
2020-07-02Fix record pattern interpretation with implicit argumentsGaëtan Gilbert
We interpret `{|proj=pat|}` as `@C _ pat` instead of `C _ pat` (where the `_` stands for the parameters). Fix #12534
2020-07-02Fix Context with nonmaximplicit.Gaëtan Gilbert
Fix #12551
2020-07-02Merge PR #12572: Correctly classify variables as being unfoldable in dnet ↵Gaëtan Gilbert
patterns. Reviewed-by: SkySkimmer Reviewed-by: maximedenes
2020-06-29Merge PR #12541: Fix #12228 negative integers not accepted in ltac integer_listPierre-Marie Pédrot
Reviewed-by: ppedrot
2020-06-24Merge PR #12532: Use the unification result for eauto's eapply.Matthieu Sozeau
Reviewed-by: mattam82
2020-06-23Correctly classify variables as being unfoldable in dnet patterns.Pierre-Marie Pédrot
Fixes #12571.
2020-06-23Add a test for the strange behaviour encountered with this change.Pierre-Marie Pédrot
2020-06-18Fix #12228 negative integers not accepted in ltac integer_listPierre Roux
2020-06-17Fix glob_sort_family for SPropGaëtan Gilbert
Fixes #12529
2020-06-08Fix 12483Pierre Roux
2020-06-06Fix uncaught NotArity in inductive typeGaëtan Gilbert
Fixes #12390
2020-05-29Fixes #12418 (inference of return clause meets assert false).Hugo Herbelin
This is a quick fix to avoid the anomaly, with a fallback on before b1b8243b7fc.
2020-05-25Merge PR #12366: Delay evaluating arguments of the "exists" tacticPierre-Marie Pédrot
Reviewed-by: ppedrot
2020-05-22Merge PR #12295: Fixes #12233: printing environment corrupted with ↵Pierre-Marie Pédrot
eta-expansion of "match" branches Reviewed-by: gares Ack-by: ppedrot
2020-05-19Delay evaluating arguments of the "exists" tacticAttila Gáspár
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-13Fixes #12233 (wrong printing env in presence of match branches eta-expansion).Hugo Herbelin
At the same time, we propagate the correct binder relevance in detyping. Note that this would be fixed by enforcing the context of branches in the syntax of "Case".
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>
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-28 21:25:19 +0000