aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/bugs/closed
Commit message (Expand)AuthorAge
...
* 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
* 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
* Quick fix for bug #2350 (ensuring enough "red" when refine calls fix tactic).Gravatar herbelin2010-07-21
* Fix (part of) bug #2347, de Bruijn bug in Program's pretyper.Gravatar msozeau2010-06-30
* Backporting modifications to nsatz (doc + fix of bug #2328) from trunk to v8.3.Gravatar herbelin2010-06-26
* Test script for bug #1962 (that is apparently solved in 8.3+trunk :-)Gravatar letouzey2010-06-20
* add in test-suite the scripts about fsetdec bugsGravatar letouzey2010-06-18
* test for bug #2141 (include + extraction)Gravatar letouzey2010-06-16
* Fixing bug 2295 (omission of option "as" in return clause of "match" was notGravatar herbelin2010-06-13
* Fixing bug 2300 (ltac pattern-matching returning terms with concrete universes).Gravatar herbelin2010-06-13
* Addressed bug #2320 in v8.2 and v8.3 branches ("refine" problem withGravatar herbelin2010-06-13
* Fixed bug #2135 (second-order unification was raising cryptic message)Gravatar herbelin2010-06-12
* Added regression tests for bugs + miscellaneous improvementsGravatar herbelin2010-06-12
* Fixed bug # 2303 in r 13087.Gravatar msozeau2010-06-09
* Fix bug #2262: bad implicit argument number by avoiding countingGravatar msozeau2010-06-09
* Automatic introduction of names given before ":" in Lemma's andGravatar herbelin2010-06-09
* Fix bug 2307Gravatar pboutill2010-05-20
* Backporting r13007 (evar_merge wrong and costly) to V8.3 and added test.Gravatar herbelin2010-05-10
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
* Fixed bug #2999 (destruct was not refreshing universes of what it generalized *)Gravatar herbelin2010-04-20
* Propagated fix to bug 2127 (Hint Rewrite badly globalized in modules) to 8.2Gravatar herbelin2010-04-20
* Test for bug #2231 (unexpected error when using let/if over an inductiveGravatar herbelin2010-04-10
* Granting wish #2251 thanks to commit 12900 solved bug 1416.v (whichGravatar herbelin2010-04-07
* Granting wish #2251 (forbidding rewriting a term reduced to an evar)Gravatar herbelin2010-04-05
* Tests for bug report #2244 (pattern-unification with abstraction over Meta's)Gravatar herbelin2010-04-05
* Applied greenrd's patch to fix bug 2255 (injection failed toGravatar herbelin2010-03-27
* bugs/.../1784.v: revert Matthieu's recent fix, since Program has been made co...Gravatar letouzey2010-02-10
* Regression test for bug #2145 (Groebner failing with "not eq" hypotheses).Gravatar herbelin2009-12-30
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-27 18:47:46 +0000