| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2015-10-21 | Removing 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-09 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 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 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 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-29 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2015-07-28 | Tests for bugs #3509 and #3510. | Pierre-Marie Pédrot | |
| 2015-07-18 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2015-07-16 | Remove old test file for #3819 (now fixed). | Maxime Dénès | |
| 2015-07-06 | Temporarily disable test file for #3922. | Maxime Dénès | |
| 2015-06-29 | Fix test file for #4214 which was fixed by Hugo. | Maxime Dénès | |
| 2015-06-29 | Better test case by PMP for #3948. | Maxime Dénès | |
| 2015-06-01 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 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-15 | Merge v8.5 into trunk | Hugo 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-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-05-05 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 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-30 | Merge branch 'v8.5' into trunk | Enrico Tassi | |
| 2015-03-24 | Updating test-suite (see previous commit). | Hugo Herbelin | |
| 2015-03-11 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 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-04 | Merge branch 'v8.5' | 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-28 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 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 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 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-23 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2015-02-21 | Moving test for bug #3071. | Pierre-Marie Pédrot | |
| 2015-02-21 | Removed tests for #3900 and #3944 as open bugs. | Hugo Herbelin | |
| 2015-02-15 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2015-02-15 | Test for bug #3490. | Pierre-Marie Pédrot | |
| 2015-02-13 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2015-02-11 | Adding test for bug #3786. | Pierre-Marie Pédrot | |
| 2015-01-28 | Several reproduction cases for the test suite. | Xavier Clerc | |
| 2015-01-28 | Several reproduction cases for the test suite. | Xavier Clerc | |
| 2015-01-18 | Revert "Update test for #3363 now that Require is forbidden inside modules." | Maxime Dénès | |
| This reverts commit 1c6e7d3744d101124ed0152c2aac1e71c9f9d40d. | |||
| 2015-01-17 | Revert "Update test for #3363 now that Require is forbidden inside modules." | Maxime Dénès | |
| This reverts commit 1c6e7d3744d101124ed0152c2aac1e71c9f9d40d. | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |