aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite
Commit message (Collapse)AuthorAge
* Improving evar restriction (this is a risky change, as I remember aGravatar Hugo Herbelin2014-12-07
| | | | | | | | similar optimization broke at some time some ssreflect code; we now treat the easy case of a let-in to a rel - a pattern common in pattern-matching compilation -; later on, we shall want to investigate whether any let-in found to refer to out of scope rels or vars can be filtered out).
* Commits on evar-evar unification fixed HoTT_coq_106 and improved theGravatar Hugo Herbelin2014-12-05
| | | | | status of #3278 (more precisely, it fixed a bug visible in the #3278 report, but a bug which arrived after #3278 was submitted).
* Take benefit of improved name preservation of evars in e2fa65fcc.Gravatar Hugo Herbelin2014-12-04
|
* Updading test-suite.Gravatar Hugo Herbelin2014-12-03
|
* When solving ?id{args} = ?id'{args'}, give preference to ?id:=?id' ifGravatar Hugo Herbelin2014-12-02
| | | | | | | | | | | possible, which is the "natural" way to orient an equation. At least it matters for matching subterms against patterns, so that it is the pattern variables which are substituted if ever the subterm has itself existential variables, as in: Goal exists x, S x = x. eexists. destruct (S _).
* Fixing test-suite.Gravatar Pierre-Marie Pédrot2014-12-01
|
* Adding test for bug #3417.Gravatar Pierre-Marie Pédrot2014-11-30
|
* Test for bug #3485.Gravatar Pierre-Marie Pédrot2014-11-30
|
* Test for bug #3487.Gravatar Pierre-Marie Pédrot2014-11-30
|
* Test of bug #3682.Gravatar Pierre-Marie Pédrot2014-11-30
|
* Fix test flags for fake_ideGravatar Enrico Tassi2014-11-27
|
* Bug #3804 is actually closed (thanks to Jason Gross for the notification).Gravatar Xavier Clerc2014-11-25
|
* Tweak some test cases.Gravatar Xavier Clerc2014-11-25
|
* Adapting to current semantics of "simpl non-evaluable-cst"Gravatar Hugo Herbelin2014-11-25
|
* Experimenting using unification when matching evar/meta free subtermsGravatar Hugo Herbelin2014-11-25
| | | | | | | | | | | | | | while before these were supposed to consider only syntactically. Made the experiment to unify with all delta flags unset. Keeping the same flags as for non evar/meta free subterms would lead to too much successes, as e.g. "true && b" matching "b" when the modulo_conv_on_closed_terms flag is set, which is the case for rewrite. But maybe should we instead investigate to have the same flags but with the restrict_conv_on_strict_subterms flag set. This rules out examples like "true && b" unifying with "b" and this is another option which is ok for compiling the stdlib without any changes.
* Adding test for bug #3248.Gravatar Pierre-Marie Pédrot2014-11-24
|
* Pass around information on the use of template polymorphism forGravatar Matthieu Sozeau2014-11-23
| | | | | | | inductive types (i.e., ones declared with an explicit anonymous Type at the conclusion of their arity). With this change one can force inductives to live in higher universes even in the non-fully universe polymorphic case (e.g. bug #3821).
* Test for closed #2713 and #2876.Gravatar Hugo Herbelin2014-11-22
|
* Add test-suite file for dependent rewriting example by Vadim Zaliva andGravatar Matthieu Sozeau2014-11-22
| | | | Daniel Schepler.
* Adding test for bug #3326.Gravatar Pierre-Marie Pédrot2014-11-21
|
* Adding test for bug #3424.Gravatar Pierre-Marie Pédrot2014-11-21
|
* Cleaning up closed bugs in test-suite.Gravatar Pierre-Marie Pédrot2014-11-21
|
* Test for bug #3788.Gravatar Pierre-Marie Pédrot2014-11-21
|
* Add test-suite file for bug #3804.Gravatar Matthieu Sozeau2014-11-21
|
* Adding test for bug #3684.Gravatar Pierre-Marie Pédrot2014-11-20
|
* Fixing a little bug with nested but convertible occurrences in "destruct at".Gravatar Hugo Herbelin2014-11-18
|
* Fixing detection of occurrences in the presence of nested subterms forGravatar Hugo Herbelin2014-11-18
| | | | "simpl at" and "change at".
* Enforcing a stronger difference between the two syntaxes "simplGravatar Hugo Herbelin2014-11-16
| | | | | | | | | | | | | | | | | | | | | | | | | | | reference" and "simpl pattern" in the code (maybe we should have merged them instead, but I finally decided to enforce their difference, even if some compatibility is to be preversed - the idea is that at some time "simpl reference" would only call a weak-head simpl (or eventually cbn), leading e.g. to reduce 2+n into S(1+n) rather than S(S(n)) which could be useful for better using induction hypotheses. In the process we also implement the following: - 'simpl "+"' is accepted to reduce all applicative subterms whose head symbol is written "+" (in the toplevel scope); idem for vm_compute and native_compute - 'simpl reference' works even if reference has maximally inserted implicit arguments (this solves the "simpl fst" incompatibility) - compatibility of ltac expressions referring to vm_compute and native_compute with functor application should now work (i.e. vm_compute and native_compute are now taken into account in tacsubst.ml) - for compatibility, "simpl eq" (assuming no maximal implicit args in eq) or "simpl @eq" to mean "simpl (eq _ _)" are still allowed. By the way, is "mul" on nat defined optimally? "3*n" simplifies to "n+(n+(n+0))". Are there some advantages of this compared to have it simplified to "n+n+n" (i.e. to "(n+n)+n").
* Fixing side bug in db37c9f3f32ae7 delaying interpretation of theGravatar Hugo Herbelin2014-11-16
| | | | | right-hand side of a "change with": the rhs lives in the toplevel environment.
* Use return code to classify anomalies as active open bugs.Gravatar Xavier Clerc2014-11-14
|
* Add missing "Fail" to test case for bug #2814.Gravatar Xavier Clerc2014-11-14
|
* Reproduction cases for the test suite.Gravatar Xavier Clerc2014-11-14
|
* Preserving the good effect of 014e5ac92a on not leaving dangling localGravatar Hugo Herbelin2014-11-14
| | | | | | definitions while keeping some compatibility on when to generalize when an index also occur in a parameter (effect on PersistentUnionFind for instance).
* Removing yet another source of remaining local definitions.Gravatar Hugo Herbelin2014-11-13
|
* Adapting output tests to current naming of evars, even if unclearGravatar Hugo Herbelin2014-11-11
| | | | where it will eventually stabilize.
* Adding test for bug 3792.Gravatar Pierre-Marie Pédrot2014-11-09
|
* Follow up to experimental eager evar unification in bcba6d1bc9:Gravatar Hugo Herbelin2014-11-08
| | | | | | | | | Observing that systematic eager evar unification makes unification works better, for instance in setoid rewrite (ATBR, SemiRing.v), we add a new flag use_evars_eagerly_in_conv_on_closed_terms which is put to true only in Rewrite.rewrite_core_unif_flags (empirically, this makes the "rewrite" from rewrite.ml working again on examples which were previously treated by use_metas_eagerly_in_conv_on_closed_terms).
* Compatibility with 8.4 in the heuristic used to build the inductionGravatar Hugo Herbelin2014-11-08
| | | | | hypothesis when indices also occur among parameters. This solves current failure of PersistentUnionFind.
* Test #3655 was failing due to an anomaly. Now it rather has to failGravatar Hugo Herbelin2014-11-08
| | | | normally, so failure is now detected by removing the "Fail".
* Test fixed by PMP's commits from Oct 21.Gravatar Hugo Herbelin2014-11-08
|
* Test for #3675 on primitive projections.Gravatar Hugo Herbelin2014-11-07
|
* Fixing #3562 ("as" in "destruct" expects either a disjunctiveGravatar Hugo Herbelin2014-11-07
| | | | intropattern or a bound ltac variable).
* Test for #3542 fixed some time ago.Gravatar Hugo Herbelin2014-11-07
|
* Consequence of changing the definition of Nat.shiftl and Nat.shiftr.Gravatar Hugo Herbelin2014-11-06
|
* Restoring clear_flag (thanks a lot to jonikelee to notice it).Gravatar Hugo Herbelin2014-11-06
|
* Optimizing when to clear generalized hypotheses in destruct.Gravatar Hugo Herbelin2014-11-06
| | | | | | Removing blocking of generalization on destructed hypothesis introduced on Nov 2. It was a bad idea as shown by bug #3790 on eliminating v:Vector n, keeping an equality.
* Test for bug #3723 and #3787 on reinitialization of empty camlp4/5 levels.Gravatar Hugo Herbelin2014-11-06
|
* Removing "destruct" test not yet working.Gravatar Hugo Herbelin2014-11-06
|
* test suite: some reproduction cases for recently-reported bugs.Gravatar Xavier Clerc2014-11-04
|
* Test for bug #2149.Gravatar Pierre-Marie Pédrot2014-11-04
|