aboutsummaryrefslogtreecommitdiff
path: root/test-suite/bugs/opened
AgeCommit message (Expand)Author
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
2015-10-21Removing test for bug #3956.Pierre-Marie Pédrot
2015-10-09Merge branch 'v8.5'Pierre-Marie Pédrot
2015-10-07Univs: add Strict Universe Declaration option (on by default)Matthieu Sozeau
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 test-su...Pierre-Marie Pédrot
2015-05-18Tentative fix for #3461: Anomaly: Uncaught exception Pretype_errors.PretypeEr...Pierre-Marie Pédrot
2015-05-15Merge v8.5 into trunkHugo Herbelin
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
2015-05-05Merge branch 'v8.5'Pierre-Marie Pédrot
2015-04-22Tactical `progress` compares term up to potentially equalisable universes.Arnaud Spiwack
2015-03-30Merge branch 'v8.5' into trunkEnrico Tassi
2015-03-24Updating test-suite (see previous commit).Hugo Herbelin
2015-03-11Merge branch 'v8.5'Pierre-Marie Pédrot
2015-03-11admit: replaced by give_up + Admitted (no proof_admitted : False, close #4032)Enrico Tassi
2015-03-08Test for bug #2951.Pierre-Marie Pédrot
2015-03-04Merge branch 'v8.5'Pierre-Marie Pédrot
2015-03-03Fix test-suite file, this is open.Matthieu Sozeau
2015-03-03Add missing test-suite files and update gitignore.Matthieu Sozeau
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-05 20:31:21 +0000