| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2015-12-02 | Changing syntax "$(tactic)$" into "ltac:(tactic)", as discussed in WG. | Hugo Herbelin | |
| 2015-11-11 | Now closed. | Matthieu Sozeau | |
| 2015-10-07 | Univs: 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-02 | Univs: fixed 3685 by side-effect :) | Matthieu Sozeau | |
| 2015-10-02 | Univs: fix test-suite file for HoTT/coq bug #120 | Matthieu Sozeau | |
| 2015-07-28 | Tests for bugs #3509 and #3510. | Pierre-Marie Pédrot | |
| 2015-07-16 | Remove old test file for #3819 (now fixed). | Maxime Dénès | |
| 2015-05-18 | Removing test for opened bugs that were already present in the closed ↵ | Pierre-Marie Pédrot | |
| test-suite. | |||
| 2015-05-18 | Tentative 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-09 | Adjusting test-suite after 5cbc018fe9347 (subst as in 8.4 by default). | Hugo Herbelin | |
| 2015-05-09 | Adding a flag "Set Regular Subst Tactic" off by default in v8.5 for | Hugo Herbelin | |
| preserving compatibility of subst after #4214 being solved. | |||
| 2015-04-22 | Tactical `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-24 | Updating test-suite (see previous commit). | Hugo Herbelin | |
| 2015-03-11 | admit: 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-08 | Test for bug #2951. | Pierre-Marie Pédrot | |
| 2015-03-03 | Fix test-suite file, this is open. | Matthieu Sozeau | |
| 2015-03-03 | Add missing test-suite files and update gitignore. | Matthieu Sozeau | |
| 2015-02-27 | Fix test for #3848, still open. | Maxime Dénès | |
| 2015-02-27 | Moving test for #3467 to closed after PMP's fix. | Maxime Dénès | |
| 2015-02-27 | Fix test-suite files for bugs #2456 and #3593, still open. | Maxime Dénès | |
| 2015-02-27 | Moving tests for #2456 and #3593 to "opened" until they're fixed. | Maxime Dénès | |
| 2015-02-27 | Moving test of #3848 to "opened". | Maxime Dénès | |
| 2015-02-26 | Test for bug #3298. | Pierre-Marie Pédrot | |
| 2015-02-26 | Moving test for bug #3681 as closed. | Pierre-Marie Pédrot | |
| 2015-02-21 | Moving test for bug #3071. | Pierre-Marie Pédrot | |
| 2015-02-15 | Test for bug #3490. | Pierre-Marie Pédrot | |
| 2015-02-11 | Adding test for bug #3786. | Pierre-Marie Pédrot | |
| 2015-01-17 | Revert "Update test for #3363 now that Require is forbidden inside modules." | Maxime Dénès | |
| This reverts commit 1c6e7d3744d101124ed0152c2aac1e71c9f9d40d. | |||
| 2015-01-12 | Update test for #3363 now that Require is forbidden inside modules. | Maxime Dénès | |
| 2014-12-19 | Fixing wrong notation level in #3295. | Hugo Herbelin | |
| 2014-12-16 | #3828 is solved. | Hugo Herbelin | |
| 2014-12-16 | Moving #2447 (congruence) to fixed. | Hugo Herbelin | |
| 2014-12-11 | New reproduction cases for the test suite. | Xavier Clerc | |
| 2014-12-05 | Commits on evar-evar unification fixed HoTT_coq_106 and improved the | Hugo 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-30 | Adding test for bug #3417. | Pierre-Marie Pédrot | |
| 2014-11-30 | Test for bug #3487. | Pierre-Marie Pédrot | |
| 2014-11-30 | Test of bug #3682. | Pierre-Marie Pédrot | |
| 2014-11-25 | Bug #3804 is actually closed (thanks to Jason Gross for the notification). | Xavier Clerc | |
| 2014-11-25 | Tweak some test cases. | Xavier Clerc | |
| 2014-11-24 | Adding test for bug #3248. | Pierre-Marie Pédrot | |
| 2014-11-21 | Cleaning up closed bugs in test-suite. | Pierre-Marie Pédrot | |
| 2014-11-14 | Add missing "Fail" to test case for bug #2814. | Xavier Clerc | |
| 2014-11-14 | Reproduction cases for the test suite. | Xavier Clerc | |
| 2014-11-08 | Test #3655 was failing due to an anomaly. Now it rather has to fail | Hugo Herbelin | |
| normally, so failure is now detected by removing the "Fail". | |||
| 2014-11-08 | Test fixed by PMP's commits from Oct 21. | Hugo Herbelin | |
| 2014-11-04 | test suite: some reproduction cases for recently-reported bugs. | Xavier Clerc | |
| 2014-11-03 | New bugs revealed fixed: #3408 by (probably) Maxime's commits | Hugo Herbelin | |
| on vm and #3068 by Nov 2 commit on destruct. Also fixed test for failure of #3459. | |||
| 2014-10-21 | More precise test for #3459. | Hugo Herbelin | |
| 2014-10-16 | Bug fixed by Hugo. | Matthieu Sozeau | |
| 2014-10-15 | Adding a timeout to bug #2447. | Pierre-Marie Pédrot | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |