aboutsummaryrefslogtreecommitdiff
path: root/test-suite/bugs/opened
AgeCommit message (Collapse)Author
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-02Changing syntax "$(tactic)$" into "ltac:(tactic)", as discussed in WG.Hugo Herbelin
2015-11-11Now closed.Matthieu Sozeau
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-02Univs: fixed 3685 by side-effect :)Matthieu Sozeau
2015-10-02Univs: fix test-suite file for HoTT/coq bug #120Matthieu Sozeau
2015-07-28Tests for bugs #3509 and #3510.Pierre-Marie Pédrot
2015-07-16Remove old test file for #3819 (now fixed).Maxime Dénès
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-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-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-24Updating test-suite (see previous commit).Hugo Herbelin
2015-03-11admit: replaced by give_up + Admitted (no proof_admitted : False, close #4032)Enrico Tassi
- no more inconsistent Axiom in the Prelude - STM can now process Admitted proofs asynchronously - the quick chain can stock "Admitted" jobs in .vio files - the vio2vo step checks the jobs but does not stock the result in the opaque tables (they have no slot) - Admitted emits a warning if the proof is complete - Admitted uses the (partial) proof term to infer section variables used (if not given with Proof using), like for Qed - test-suite: extra line Require TestSuite.admit to each file making use of admit - test-suite/_CoqProject: to pass to CoqIDE and PG the right -Q flag to find TestSuite.admit
2015-03-08Test for bug #2951.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
2015-02-27Fix test for #3848, still open.Maxime Dénès
2015-02-27Moving test for #3467 to closed after PMP's fix.Maxime Dénès
2015-02-27Fix test-suite files for bugs #2456 and #3593, still open.Maxime Dénès
2015-02-27Moving tests for #2456 and #3593 to "opened" until they're fixed.Maxime Dénès
2015-02-27Moving test of #3848 to "opened".Maxime Dénès
2015-02-26Test for bug #3298.Pierre-Marie Pédrot
2015-02-26Moving test for bug #3681 as closed.Pierre-Marie Pédrot
2015-02-21Moving test for bug #3071.Pierre-Marie Pédrot
2015-02-15Test for bug #3490.Pierre-Marie Pédrot
2015-02-11Adding test for bug #3786.Pierre-Marie Pédrot
2015-01-17Revert "Update test for #3363 now that Require is forbidden inside modules."Maxime Dénès
This reverts commit 1c6e7d3744d101124ed0152c2aac1e71c9f9d40d.
2015-01-12Update test for #3363 now that Require is forbidden inside modules.Maxime Dénès
2014-12-19Fixing wrong notation level in #3295.Hugo Herbelin
2014-12-16#3828 is solved.Hugo Herbelin
2014-12-16Moving #2447 (congruence) to fixed.Hugo Herbelin
2014-12-11New reproduction cases for the test suite.Xavier Clerc
2014-12-05Commits on evar-evar unification fixed HoTT_coq_106 and improved theHugo Herbelin
status of #3278 (more precisely, it fixed a bug visible in the #3278 report, but a bug which arrived after #3278 was submitted).
2014-11-30Adding test for bug #3417.Pierre-Marie Pédrot
2014-11-30Test for bug #3487.Pierre-Marie Pédrot
2014-11-30Test of bug #3682.Pierre-Marie Pédrot
2014-11-25Bug #3804 is actually closed (thanks to Jason Gross for the notification).Xavier Clerc
2014-11-25Tweak some test cases.Xavier Clerc
2014-11-24Adding test for bug #3248.Pierre-Marie Pédrot
2014-11-21Cleaning up closed bugs in test-suite.Pierre-Marie Pédrot
2014-11-14Add missing "Fail" to test case for bug #2814.Xavier Clerc
2014-11-14Reproduction cases for the test suite.Xavier Clerc
2014-11-08Test #3655 was failing due to an anomaly. Now it rather has to failHugo Herbelin
normally, so failure is now detected by removing the "Fail".
2014-11-08Test fixed by PMP's commits from Oct 21.Hugo Herbelin
2014-11-04test suite: some reproduction cases for recently-reported bugs.Xavier Clerc
2014-11-03New bugs revealed fixed: #3408 by (probably) Maxime's commitsHugo Herbelin
on vm and #3068 by Nov 2 commit on destruct. Also fixed test for failure of #3459.
2014-10-21More precise test for #3459.Hugo Herbelin
2014-10-16Bug fixed by Hugo.Matthieu Sozeau
generated by cgit v1.2.3 (git 2.25.1) at 2026-10-07 12:54:11 +0000