| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2014-10-15 | Fix test-suite files which failed due to usage of $(admit)$ which | Matthieu Sozeau | |
| now fails with Error: Already an existential evar of name Main | |||
| 2014-10-15 | Fix bug 3637. | Matthieu Sozeau | |
| 2014-10-15 | Reenable FO unification of primitive projections and their eta-expanded | Matthieu Sozeau | |
| forms in evarconv and unification, as well as fallback to first-order unification when eta for constructors fail. Update test-suite file 3484 to test for the FO case in evarconv as well. | |||
| 2014-10-15 | Fix test-suite file after moving back to using C as the name | Matthieu Sozeau | |
| of the record binder for Class C's projections. | |||
| 2014-10-15 | Implement a different strategy to expand primitive projections only when | Matthieu Sozeau | |
| required, i.e. in first-order unification cases where the head of the other side is a hole or the eta-expanded constant. | |||
| 2014-10-14 | Fix bug #3698: stack overflow due to eta+canonical structures in | Matthieu Sozeau | |
| unification. | |||
| 2014-10-08 | Fixing the anomaly in bug #3045 (a filter was not type-safe in | Hugo Herbelin | |
| 2nd-order matching). We made the filter type-safe (i.e. to ensure that Gamma |- ?n:T is well-typed when taking the filtered context Gamma) in 2nd order matching. Maybe this weakens the power of the 2nd order matching algorithm, so it is not clear that it is the good fix. Another fix could have been to ensure that taking the closure of filter does not extend it beyond the original filter (hence keeping the filter untyped if it was already untyped). As for the bug #3045, it also revealed that some "destruct c as [[]]" could be made stronger as decomposing the destruct in two parts "destruct c as [x]; destruct x" workis while it currently fails if in one part. | |||
| 2014-10-07 | Add test-suite file for the projection unfolding bug I just fixed. | Matthieu Sozeau | |
| 2014-10-07 | Fix test-suite file 3352 which was containing the wrong test. | Matthieu Sozeau | |
| 2014-10-07 | Fix test-suite file to test original bug, not the failure of the guard | Matthieu Sozeau | |
| condition. | |||
| 2014-10-03 | Fixing #3657 (check that both sides of a "change with" have the same | Hugo Herbelin | |
| type, what is necessary condition to ensure that the conversion of bodies will not raise an anomaly). | |||
| 2014-10-03 | Test for bug #3652 fixed in 0fb36157b9ba | Hugo Herbelin | |
| 2014-10-03 | Fixing #3623 (unbound evars in types in a call to "change with"). | Hugo Herbelin | |
| 2014-10-02 | Implement module subtyping for polymorphic constants (errors on | Matthieu Sozeau | |
| inductives). The implementation constant should have the a universe instance of the same length, we assume the universes are in the same order and we check that the definition does not add any constraints to the expected ones. This fixes bug #3670. | |||
| 2014-10-02 | Fixing bug #2810 (autounfold on local variable declared as hint but cleared). | Hugo Herbelin | |
| 2014-10-01 | Removing test for bug #2080. | Pierre-Marie Pédrot | |
| Naming a Ltac definition like a built-in tactic used to fail, but now only spits out a warning. This is too complicated to test... | |||
| 2014-09-30 | Add a bunch of reproduction files for closed bugs. | Xavier Clerc | |
| 2014-09-29 | Bug fixed. | Matthieu Sozeau | |
| 2014-09-29 | Fix test-suite files | Matthieu Sozeau | |
| 3566 gave a legitimate error, keyedrewrite was not setting keyed unification on. | |||
| 2014-09-29 | In evarconv and unification, expand folded primitive projections to | Matthieu Sozeau | |
| their eta-expanded forms which can then unfold back to the unfolded primitive projection form. This removes all special code that was necessary to handle primitive projections before, while keeping compatibility. Also fix cbn which was not refolding primitive projections correctly in all cases. Update some test-suite files accordingly. | |||
| 2014-09-27 | Fix test-suite file. | Matthieu Sozeau | |
| 2014-09-27 | Fix bug #3664 by refolding projections that don't reduce in cbn. | Matthieu Sozeau | |
| 2014-09-27 | Fix semantics of matching with folded/unfolded projections to definitely | Matthieu Sozeau | |
| avoid looping and be compatible with unfold. | |||
| 2014-09-27 | Fix bug #3672, application of primitive projections as coercions. | Matthieu Sozeau | |
| 2014-09-27 | Fix bug 3662 by actually reducing primitive projections in cbv/compute. | Matthieu Sozeau | |
| 2014-09-27 | Bug fixed. | Matthieu Sozeau | |
| 2014-09-27 | Make pattern_of_constr typed so that we can infer the proper patterns | Matthieu Sozeau | |
| for primitive projections, fixing bug #3661. Also fix expand_projection so that it does enough reduction to find the inductive type of its argument. | |||
| 2014-09-26 | Fix canonical structure resolution which was launched on the results of | Matthieu Sozeau | |
| eta-expansion, creating a loop. This is now deactivated. Fixes bugs #3665 and #3667. | |||
| 2014-09-26 | Bug #3566 is fixed. | Xavier Clerc | |
| 2014-09-26 | Adding a test for bug #3653. | Pierre-Marie Pédrot | |
| 2014-09-26 | Test cases for closed bugs. | Xavier Clerc | |
| 2014-09-25 | Add several reproduction files for bugs. | Xavier Clerc | |
| 2014-09-24 | Update test-suite files. | Matthieu Sozeau | |
| 2014-09-23 | Fix bug #3656. | Matthieu Sozeau | |
| Maintain the user-level view of primitive projections, disallow manual unfolding and do not let hnf give the eta-expanded form. | |||
| 2014-09-19 | Move the specific map_constr_with_binders_left_to_right | Matthieu Sozeau | |
| for e_contextually where it is used. Bug #3648 is fixed. | |||
| 2014-09-18 | Fix constrMatching as well as change/e_contextually to allow | Matthieu Sozeau | |
| matching partial applications of primitive projections. Fixes bug #3637. | |||
| 2014-09-18 | Fix debug printing with primitive projections. | Matthieu Sozeau | |
| Add a flag to indicate if we're in the toplevel or debuggger to not try to retype terms in the wrong environment (and making find_rectype, get_type_of untraceable). This fixes bug #3638 along with the previous commit. | |||
| 2014-09-17 | Fix bug #3593, making constr_eq and progress work up to | Matthieu Sozeau | |
| equality of universes, along with a few other functions in evd. | |||
| 2014-09-17 | Fix bug #3633 properly, by delaying the interpetation of constrs in | Matthieu Sozeau | |
| apply f, g,... so that apply f, g. succeeds when apply f; apply g does. It just mimicks the behavior of rewrite foo bar. | |||
| 2014-09-17 | Revert "While resolving typeclass evars in clenv, touch only the ones that ↵ | Matthieu Sozeau | |
| appear in the" This reverts commit 9de1edd730eeb3cada742a27a36bc70178eda6d8. Not the right way to do it. The evd shouldn't contain unrelated evars in the first place. | |||
| 2014-09-17 | While resolving typeclass evars in clenv, touch only the ones that appear in the | Matthieu Sozeau | |
| clenv's value and type, ensuring we don't try to solve unrelated goals (fixes bug#3633). | |||
| 2014-09-17 | Update test-suite files after last commit. Add a file for rewrite_strat | Matthieu Sozeau | |
| examples. | |||
| 2014-09-17 | Revert specific syntax for primitive projections, avoiding ugly | Matthieu Sozeau | |
| contortions in internalization/externalization. It uses a fully typed version of detyping, requiring the environment, to move from primitive projection applications to regular applications of the eta-expanded version. The kernel is unchanged, and only constrMatching needs compatibility code now. | |||
| 2014-09-15 | Fixing line break in test for #3559. | Hugo Herbelin | |
| 2014-09-13 | Fixing injection bug #3616 on sigma-types. | Hugo Herbelin | |
| 2014-09-12 | An old typo which was preventing example #3537 to work the same as it | Hugo Herbelin | |
| was working in 8.4. | |||
| 2014-09-11 | Fix test-suite files, and move some opened to closed. | Matthieu Sozeau | |
| 2014-09-11 | Fix bug #3594: eta for constructors and functions at the same time which | Matthieu Sozeau | |
| was failing in this case due to the wrong postponment of an unsolvable ?X = RigidContext[?X] problem. | |||
| 2014-09-11 | Fix bug #3596, wrong treatment of projections in compute_constelim_direct. | Matthieu Sozeau | |
| 2014-09-11 | Fix bug #3505. | Matthieu Sozeau | |
| When w_unifying primitive projection applications, force the unification of types of the projected records to recover instances for the parameters (evarconv does this automatically by unifying evar instances with their expected type). | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |