aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/bugs
Commit message (Expand)AuthorAge
* Fixing #2836 (materialize_evar might refine as a side effect theGravatar herbelin2012-07-29
* Continuing r15459: it helps testing occur-check early in someGravatar herbelin2012-07-06
* ZArith + other : favor the use of modern names instead of compat notationsGravatar letouzey2012-07-05
* Fixing bug #2817 (occur check was not done up to instantiation ofGravatar herbelin2012-06-20
* Implicit arguments of Definition are taken from the type when given by the user.Gravatar pboutill2012-04-27
* Bug 2733 : { } implicits and FixpointsGravatar pboutill2012-04-17
* Fixing tauto "special" behavior on singleton types w/ 2 parameters (bug #2680).Gravatar herbelin2012-04-15
* Repair two testsGravatar letouzey2012-04-12
* Generalized the use of evar candidates in type inference unification:Gravatar herbelin2012-03-20
* Fix bugs related to Program integration.Gravatar msozeau2012-03-19
* Fixing bug #2732 (anomaly when using the tolerance for writingGravatar herbelin2012-03-18
* Fixing vm_compute bug #2729 (function used to decompose constructorsGravatar herbelin2012-03-13
* Backtracking on r14876 (fix for bug #2267): extra scopes might beGravatar herbelin2012-01-05
* Fixing Arguments Scope bug when too many scopes are given (bug #2667).Gravatar herbelin2012-01-04
* Extend the computation of dependencies in pattern-matching compilationGravatar herbelin2011-11-21
* Fixing bug #2640 and variants of it (inconsistency between when andGravatar herbelin2011-11-17
* Fixing bug #1834 (de Bruijn indices bug in pattern-matching compilation).Gravatar herbelin2011-11-16
* Regression tests for bugs #2613 and #2616.Gravatar herbelin2011-10-25
* New strategy to infer return predicate of match construct whenGravatar herbelin2011-10-25
* Mod_subst: Attempt to fix #2608Gravatar letouzey2011-10-24
* Fix bug #2473 due to wrong folding of the evar environmentGravatar msozeau2011-10-18
* Fix inductive coercion code in Program (bug #2378)Gravatar msozeau2011-10-18
* Fix bug #2586 and enhance clsubst* as well as a side effectGravatar msozeau2011-10-18
* Fix bug #2456 and wrong unfolding of lets in the goal due to [unfold] doing z...Gravatar msozeau2011-10-17
* test-suite: non-regression test for bug #2603Gravatar letouzey2011-10-12
* Added test for bug #2615Gravatar herbelin2011-10-11
* fsetdec : non-atomic elements are now transformed as variables first (fix #2464)Gravatar letouzey2011-10-07
* Improved handling of element equalities in fsetdec (fix #2467)Gravatar letouzey2011-10-07
* Omega aware of Z.pred (fix #1912)Gravatar letouzey2011-09-15
* Re-allowing assumptions during proofs seems safe now (fix #2411)Gravatar letouzey2011-09-15
* Relaxed the constraint introduced in r14190 that froze the existingGravatar herbelin2011-06-18
* r14204 and 14218 continued: completely removing test for bug #2490,Gravatar herbelin2011-06-18
* Partial backtrack on wrong r14204: bug #2490 still open.Gravatar herbelin2011-06-18
* Regression files for bugs #2304 and #2490.Gravatar herbelin2011-06-14
* Fixing bug #2181 (Class mechanism can create dependencies over unnamedGravatar herbelin2011-06-14
* Test for bug 462 and 2342 fixed by Matthieu's 13990 (or so).Gravatar herbelin2011-05-15
* Merge branch 'subclasses' into coq-trunkGravatar msozeau2011-05-05
* Some fixes of the test-suite scriptsGravatar letouzey2011-02-21
* Correct handling of existential variables when multiple differentGravatar msozeau2011-02-08
* Adding test-case for bug #2362, which uses HO unification duringGravatar msozeau2010-10-12
* Fix bug #2393: allow let-ins inside telescopes (only fails when there'sGravatar msozeau2010-10-12
* Backporting r13521 from branch 8.3 to trunk (fixing bug #2406, loopingGravatar herbelin2010-10-11
* Fixed test of bug #2360 (use of Fail to check a regular error insteadGravatar herbelin2010-09-20
* Fixing bug #2360 (descend_in_conjunctions built ill-typed terms). Shouldn't weGravatar herbelin2010-09-19
* Fixing bugs #2347 (part 2) and #2388: error message printing was doneGravatar herbelin2010-09-18
* fixed bug #2375 (congruence)Gravatar corbinea2010-09-02
* Updated test on Nsatz after Loïc moved NsatzR to Nsatz.Gravatar herbelin2010-07-30
* test-case for bug #2105Gravatar barras2010-07-29
* fixed bug #2139: compiled cofix loops, missing offset to evaluate cofix bodiesGravatar barras2010-07-28
* Backporting fix to bug #2353 (fixpoint with recursively non-uniformGravatar herbelin2010-07-21
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-28 13:00:04 +0000