| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2016-10-27 | Fixing #5161 (case of a notation with unability to detect a recursive binder). | Hugo Herbelin | |
| Type annotations in unrelated binders were badly interfering with detection of recursive binders in notations. | |||
| 2016-10-25 | Merge remote-tracking branch 'github/pr/329' into v8.5 | Maxime Dénès | |
| Was PR#329: Fix #5127 Memory corruption with the VM | |||
| 2016-10-24 | Test file for #5127: Memory corruption with the VM | Maxime Dénès | |
| 2016-10-24 | Fixing #3479 (parsing of "{" and "}" when a keyword starts with "{" or "}"). | Hugo Herbelin | |
| 2016-10-24 | Fix 6d5fe92e to #5150 (missing dependencies in test suite) was a bit too strong. | Hugo Herbelin | |
| New fix. A bit less consistent with the spirit of this Makefile as we list prerequisite files explicitly, but avoid to redo subsystems at each call to "make" as with previous fix. Other solutions from experts are welcome. | |||
| 2016-10-22 | Fixing printing of generic arguments of tag "var". | Hugo Herbelin | |
| 2016-10-21 | Revert "unification.ml: fix for bug #4763, unif regression" | Maxime Dénès | |
| This reverts commit 0b417c12eb10bb29bcee04384b6c0855cb9de73a. A good fix requires to review a bit the design of unification constraint postponement, which we do in 8.6. We leave things as they are in 8.5 for compatibility. | |||
| 2016-10-20 | Adding dependency of the test-suite subsystems in prerequisite (fixing #5150). | Hugo Herbelin | |
| 2016-10-20 | A fix for #5097 (status of evars refined by "clear" in ltac: closed wrt evars). | Hugo Herbelin | |
| If an existing evar was cleared in pretyping (typically while processing "ltac:"), it created an evar considered as new. Updating them instead along the "cleared" flag. If correct, I suspect similar treatment should be done for refining along "change", "rename" and "move". | |||
| 2016-10-18 | Removing output test for module qualification. | Pierre-Marie Pédrot | |
| I do not know how to provide a proper test in 8.5, as the location on my machine appears in the error printed when loading the file. Adding a Fail on the End command does not help much either, because it simply does not print anything. Do not merge this commit in 8.6, we still want a test there. | |||
| 2016-10-17 | Fixing to #3209 (Not_found due to an occur-check cycle). | Hugo Herbelin | |
| The fix solves the original bug report but it only turns the Not_found into a normal error in the alternative example by Guillaume. See test-suite file for comments on how to eventually improve the situation and find a solution in Guillaume's example too. | |||
| 2016-10-17 | Merge PR #310 into v8.5 | Pierre-Marie Pédrot | |
| 2016-10-17 | Test for bug #4874. | Pierre-Marie Pédrot | |
| 2016-10-12 | Fixing a collision about the meta-variable ".." in recursive notations. | Hugo Herbelin | |
| This happens when recursive notations are used to define recursive notations. | |||
| 2016-10-12 | Merge remote-tracking branch 'git/bug5123' into v8.5 | Matthieu Sozeau | |
| 2016-10-11 | Fix test-suite file 5123 to fail in case of regression | Matthieu Sozeau | |
| 2016-10-11 | Fix bug #5123: mark all shelved evars unresolvable | Matthieu Sozeau | |
| Previously, some splipped through and were caught by unrelated calls to typeclass resolution. | |||
| 2016-10-11 | Fix for bug #4863, update the Proofview's env with | Matthieu Sozeau | |
| side_effects. Partial solution to the handling of side effects in proofview. | |||
| 2016-10-10 | Add test file for #4416. | Maxime Dénès | |
| 2016-10-06 | evarconv.ml: Fix bug #4529, primproj unfolding | Matthieu Sozeau | |
| Evarconv was made precociously dependent on user-declared reduction behaviors. Only cbn should rely on that. | |||
| 2016-10-06 | unification.ml: fix for bug #4763, unif regression | Matthieu Sozeau | |
| Do not force all remaining conversions problems to be solved after the _first_ solution of an evar, but only at the end of assignment of terms to evars in w_merge. This was hell to track down, thanks for the help of Maxime. contribs pass and HoTT too. | |||
| 2016-10-03 | Fixing #4970 (confusion between special "{" and non special "{{" in notations). | Hugo Herbelin | |
| 2016-09-30 | Fix test-suite. | Maxime Dénès | |
| Restore subst output test file modified by mistake. | |||
| 2016-09-30 | Merge branch '4762' into v8.5 | Maxime Dénès | |
| Was PR#293: Fix #4762 (eauto weaker than auto). | |||
| 2016-09-30 | Fix #4762. | Cyprien Mangin | |
| 2016-09-29 | Fix a bug in subst releaved by an OCaml warning. | Maxime Dénès | |
| 2016-09-22 | Fixing #5095 (non relevant too strict test in let-in abstraction). | Hugo Herbelin | |
| 2016-09-14 | Fixing test-suite after commit 43104a0b. | Pierre-Marie Pédrot | |
| 2016-09-12 | Fixing a recursive notation bug raised on coq-club on Sep 12, 2016. | Hugo Herbelin | |
| 2016-09-10 | Test for #5077. | Hugo Herbelin | |
| 2016-09-05 | Test file for #5065 - Anomaly: Not a proof by induction | Maxime Dénès | |
| 2016-09-01 | Fix test-suite after Frédéric's 6231f07b2. | Maxime Dénès | |
| 2016-08-31 | Fix bug #5043: [Admitted] lemmas pick up section variables. | Pierre-Marie Pédrot | |
| We add a flag Keep Admitted Variables that allows to recover the legacy v8.4 behaviour of admitted lemmas. The statement of such lemmas did not depend on the current context variables. | |||
| 2016-08-20 | Fixing an anomaly in printing a unification error message. | Hugo Herbelin | |
| 2016-07-29 | Fix bug #4673: regression in setoid_rewrite. | Matthieu Sozeau | |
| Modulo delta for types should be fully transparent. | |||
| 2016-07-29 | Fix bug #3886, generation of obligations of fixes | Matthieu Sozeau | |
| This partially reverts c14ccd1b8a3855d4eb369be311d4b36a355e46c1 | |||
| 2016-07-29 | Fix #4769, univ poly and elim schemes in sections | Matthieu Sozeau | |
| 2016-07-26 | Fix bug #4754, allow conversion problems to remain | Matthieu Sozeau | |
| when checking that the rewrite relation is homogeneous in setoid_rewrite. | |||
| 2016-07-20 | Fix bug #4780: universe leak in letin_tac | Matthieu Sozeau | |
| 2016-07-19 | Fix Errors.out missing a dot... | Matthieu Sozeau | |
| 2016-07-13 | Fixing printing of evar name in an error message of instantiate. | Hugo Herbelin | |
| 2016-07-08 | Fix test file for #4858. | Maxime Dénès | |
| 2016-07-08 | Update csdp.cache. | Maxime Dénès | |
| 2016-07-08 | Test file for #4858. | Maxime Dénès | |
| 2016-07-08 | Add test file for #4880. | Maxime Dénès | |
| 2016-07-06 | Update csdp.cache. | Maxime Dénès | |
| 2016-07-06 | Merge remote-tracking branch 'github/pr/199' into v8.5 | Maxime Dénès | |
| Was PR#199: Unbreak singleton list-like notation (-compat 8.4) | |||
| 2016-07-05 | congruence fix: test-suite code and update CHANGES | Matthieu Sozeau | |
| This fixes bugs #4069 (not 4609 as mentionned in the git log) and #4718. | |||
| 2016-07-04 | congruence: Restrict refreshing to Set | Matthieu Sozeau | |
| Because refreshing Prop is not semantics-preserving, the new universe is >= Set, so cannot be minimized to Prop afterwards. | |||
| 2016-07-04 | congruence/univs: properly refresh (fix #4609) | Matthieu Sozeau | |
| In congruence, refresh universes including the Set/Prop ones so that congruence works with cumulativity, not restricting itself to the inferred types of terms that are manipulated but allowing them to be used at more general types. This fixes bug #4609. | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |
path: root/test-suite