aboutsummaryrefslogtreecommitdiff
path: root/test-suite/bugs
AgeCommit message (Collapse)Author
2020-07-03Fix #11121: Simultaneous definition of term and notation in custom grammarMaxime Dénès
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>
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-27 16:54:13 +0000