aboutsummaryrefslogtreecommitdiff
path: root/test-suite/bugs/opened
AgeCommit message (Expand)Author
2021-04-02Remove the omega tactic and related optionsJim Fehrle
2021-01-04EConstr iterators respect the binding structure of cases.Pierre-Marie Pédrot
2020-10-22Remove test-suite/bugs/opened/bug_3395.v: not a bugGaëtan Gilbert
2020-08-19Adding the example of bug #2904 into the test suite, and reorganising the tes...Martin Bodin
2019-12-04Manual implicit arguments: more robustness tests.Hugo Herbelin
2019-11-25Test-suite: avoid using “omega”Vincent Laporte
2019-10-04[Stdlib] OrderedType: do not pollute the “core” hint databaseVincent Laporte
2019-05-20Remove VtUnknown classificationMaxime Dénès
2019-05-13Make detyping robust w.r.t. indexed anonymous variablesMaxime Dénès
2019-01-22Turn `Refine Instance Mode` off by defaultMaxime Dénès
2019-01-09Make some tests more robust by adding missing proof terminatorsMaxime Dénès
2019-01-08Fix #9272: `Unset Nested Proofs Allowed` does not capture nested `Instance` p...Maxime Dénès
2018-12-19Fix #7904: update proofview env after ltac constr:()Gaëtan Gilbert
2018-10-04test-suite: cleaningVincent Laporte
2018-10-04rename test files (do not start by a digit)Vincent Laporte
2018-04-12Merge PR #7179: Fix #5981, bugs/opened/3263.v is non-deterministic by removin...Jason Gross
2018-04-11Fix the status of some resolved bugsTej Chajed
2018-04-05Fix #5981, bugs/opened/3263.v is non-deterministic by removing the test.Théo Zimmermann
2018-03-30Change Implicit Arguments to Arguments in test-suiteJasper Hugunin
2018-03-08[compat] Remove "Refolding Reduction" option.Emilio Jesus Gallego Arias
2018-03-08Merge PR #6899: [compat] Remove "Standard Proposition Elimination"Maxime Dénès
2018-03-04Remove deprecated options related to typeclasses.Théo Zimmermann
2018-03-03[compat] Remove "Standard Proposition Elimination"Emilio Jesus Gallego Arias
2018-02-14Extend `zify_N` with knowledge about `N.pred`Joachim Breitner
2018-01-17Let dtauto recognize '@sigT A (fun _ => B)' as a conjunctionJasper Hugunin
2017-11-23Using is_conv rather than eq_constr to find `nat` or `Z` in omega.Hugo Herbelin
2017-10-23Move bug files to match their new GitHub ID (fixes #6001).Théo Zimmermann
2017-08-21Ensuring all .v files end with a newline to make "sed -i" work better on them.Hugo Herbelin
2017-06-14Remove support for Coq 8.4.Guillaume Melquiond
2017-05-01remove unneeded -emacs flag to coq-prog-argsPaul Steckler
2016-11-17Merge commit '633ed9c' into v8.6Maxime Dénès
2016-11-17Add test suite files for 4700-4785Jason Gross
2016-09-29Move vector/list compat notations to their relevant filesJason Gross
2016-09-29Arguments: cleanup + detect discrepancy rename/implicit (#3753)Enrico Tassi
2016-07-18Marking bug #3383 as solved.Pierre-Marie Pédrot
2016-07-18Fix bug #4923: Warning: appcontext is deprecated.Pierre-Marie Pédrot
2016-07-07Merge branch 'v8.5' into v8.6Pierre-Marie Pédrot
2016-06-15Fix test-suite for opened bug #4813.Pierre-Marie Pédrot
2016-06-12For the record, an example one would like to see working.Hugo Herbelin
2016-06-09Unbreak singleton list-like notation (-compat 8.4)Jason Gross
2016-03-19Moving the parsing of the Ltac proof mode to G_ltac.Pierre-Marie Pédrot
2016-02-22Moving the Tauto tactic to proper Ltac.Pierre-Marie Pédrot
2016-01-13Merge branch 'v8.5'Pierre-Marie Pédrot
2016-01-12Fixing #4256 and #4484 (changes in evar-evar resolution made that newHugo Herbelin
2015-12-30External tactics and notations now accept any tactic argument.Pierre-Marie Pédrot
2015-12-17Merge branch 'v8.5'Pierre-Marie Pédrot
2015-12-03Merge branch 'v8.5'Pierre-Marie Pédrot
2015-12-02Changing syntax "$(tactic)$" into "ltac:(tactic)", as discussed in WG.Hugo Herbelin
2015-11-15Merge branch 'v8.5'Pierre-Marie Pédrot
2015-11-11Now closed.Matthieu Sozeau
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 21:25:10 +0000