aboutsummaryrefslogtreecommitdiff
path: root/test-suite/bugs/opened
AgeCommit message (Collapse)Author
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
Moving at the same to a passing "env sigma" style rather than passing "gl". Not that it is strictly necessary, but since we had to move functions taking only a "sigma" to functions taking also a "env", we eventually adopted the "env sigma" style. (The "gl" style would have been as good.) This answers wish #4717.
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
Was PR#192: Add test suite files for 4700-4785
2016-11-17Add test suite files for 4700-4785Jason Gross
I didn't add any test-cases for timing-based bugs (4707, 4768, 4776, 4777, 4779, 4783), nor CoqIDE bugs (4700, 4751, 4752, 4756), nor bugs about printing (4709, 4711, 4720, 4723, 4734, 4736, 4738, 4741, 4743, 4748, 4749, 4750, 4757, 4758, 4765, 4784). I'm not sure what to do with 4712, 4714, 4732, 4740.
2016-09-29Move vector/list compat notations to their relevant filesJason Gross
Since edb55a94fc5c0473e57f5a61c0c723194c2ff414 landed, compat notations no longer modify the parser in non-compat-mode, so we can do this without breaking Ltac parsing. Also update the related test-suite files.
2016-09-29Arguments: cleanup + detect discrepancy rename/implicit (#3753)Enrico Tassi
It seems warnings are not taken into account in output/ tests.
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
With this commit, it is possible to write notations so that singleton lists are usable in both 8.4 and 8.5pl1 -compat. Longer lists await the ability to remove notations from the parser.
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
This gets rid of brittle code written in ML files through Ltac quotations, and reduces the dependance of Coq to such a feature. This also fixes the particular instance of bug #2800, although the underlying issue is still there.
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
evars were created making in turn that evars formerly recognized as pending were not anymore in the list of pending evars). This also fixes the reopening of #3848. See comments on #4484 for details.
2015-12-30External tactics and notations now accept any tactic argument.Pierre-Marie Pédrot
This commit has deep consequences in term of tactic evaluation, as it allows to pass any tac_arg to ML and alias tactics rather than mere generic arguments. This makes the evaluation much more uniform, and in particular it removes the special evaluation function for notations. This last point may break some notations out there unluckily. I had to treat in an ad-hoc way the tactic(...) entry of tactic notations because it is actually not interpreted as a generic argument but rather as a proper tactic expression instead. There is for now no syntax to pass any tactic argument to a given ML or notation tactic, but this should come soon. Also fixes bug #3849 en passant.
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
2015-10-21Removing test for bug #3956.Pierre-Marie Pédrot
It breaks test-suite of trunk since Matthieu's fixes for the soundness of polymorphic universes, and I am unsure of the expected semantics. We should reintroduce it later on when we understand better the issue of simply fix it once and for all.
2015-10-09Merge branch 'v8.5'Pierre-Marie Pédrot
2015-10-07Univs: add Strict Universe Declaration option (on by default)Matthieu Sozeau
This option disallows "declare at first use" semantics for universe variables (in @{}), forcing the declaration of _all_ universes appearing in a definition when introducing it with syntax Definition/Inductive foo@{i j k} .. The bound universes at the end of a definition/inductive must be exactly those ones, no extras allowed currently. Test-suite files using the old semantics just disable the option.
2015-10-02Merge branch 'v8.5'Pierre-Marie Pédrot
2015-10-02Univs: fixed 3685 by side-effect :)Matthieu Sozeau
2015-10-02Univs: fix test-suite file for HoTT/coq bug #120Matthieu Sozeau
2015-07-29Merge branch 'v8.5'Pierre-Marie Pédrot
2015-07-28Tests for bugs #3509 and #3510.Pierre-Marie Pédrot
2015-07-18Merge branch 'v8.5'Pierre-Marie Pédrot
2015-07-16Remove old test file for #3819 (now fixed).Maxime Dénès
2015-07-06Temporarily disable test file for #3922.Maxime Dénès
2015-06-29Fix test file for #4214 which was fixed by Hugo.Maxime Dénès
2015-06-29Better test case by PMP for #3948.Maxime Dénès
2015-06-01Merge branch 'v8.5'Pierre-Marie Pédrot
2015-05-18Removing test for opened bugs that were already present in the closed ↵Pierre-Marie Pédrot
test-suite.
2015-05-18Tentative fix for #3461: Anomaly: Uncaught exception ↵Pierre-Marie Pédrot
Pretype_errors.PretypeError. Instad of trying to print the exception, we raise it in the tactic monad.
2015-05-15Merge v8.5 into trunkHugo Herbelin
Conflicts: tactics/eauto.ml4 (merging eauto.ml4 and adapting coq_micromega.ml to new typing.ml API)
2015-05-14#3953 now closed.Hugo Herbelin
2015-05-09Adjusting test-suite after 5cbc018fe9347 (subst as in 8.4 by default).Hugo Herbelin
2015-05-09Adding a flag "Set Regular Subst Tactic" off by default in v8.5 forHugo Herbelin
preserving compatibility of subst after #4214 being solved.
2015-05-05Merge branch 'v8.5'Pierre-Marie Pédrot
2015-04-22Tactical `progress` compares term up to potentially equalisable universes.Arnaud Spiwack
Followup of: f7b29094fe7cc13ea475447bd30d9a8b942f0fef . In particular, re-closes #3593. As a side effect, fixes an undiscovered bug of the `eq_constr` tactic which didn't consider terms up to evar instantiation.
2015-03-30Merge branch 'v8.5' into trunkEnrico Tassi
2015-03-24Updating test-suite (see previous commit).Hugo Herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-02 11:14:02 +0000