aboutsummaryrefslogtreecommitdiff
path: root/test-suite/bugs/closed
AgeCommit message (Expand)Author
2011-06-14Regression files for bugs #2304 and #2490.herbelin
2011-06-14Fixing bug #2181 (Class mechanism can create dependencies over unnamedherbelin
2011-05-15Test for bug 462 and 2342 fixed by Matthieu's 13990 (or so).herbelin
2011-05-05Merge branch 'subclasses' into coq-trunkmsozeau
2011-02-21Some fixes of the test-suite scriptsletouzey
2011-02-08Correct handling of existential variables when multiple differentmsozeau
2010-10-12Adding test-case for bug #2362, which uses HO unification duringmsozeau
2010-10-12Fix bug #2393: allow let-ins inside telescopes (only fails when there'smsozeau
2010-10-11Backporting r13521 from branch 8.3 to trunk (fixing bug #2406, loopingherbelin
2010-09-20Fixed test of bug #2360 (use of Fail to check a regular error insteadherbelin
2010-09-19Fixing bug #2360 (descend_in_conjunctions built ill-typed terms). Shouldn't weherbelin
2010-09-18Fixing bugs #2347 (part 2) and #2388: error message printing was doneherbelin
2010-09-02fixed bug #2375 (congruence)corbinea
2010-07-30Updated test on Nsatz after Loïc moved NsatzR to Nsatz.herbelin
2010-07-29test-case for bug #2105barras
2010-07-28fixed bug #2139: compiled cofix loops, missing offset to evaluate cofix bodiesbarras
2010-07-21Backporting fix to bug #2353 (fixpoint with recursively non-uniformherbelin
2010-07-21Quick fix for bug #2350 (ensuring enough "red" when refine calls fix tactic).herbelin
2010-06-30Fix (part of) bug #2347, de Bruijn bug in Program's pretyper.msozeau
2010-06-26Backporting modifications to nsatz (doc + fix of bug #2328) from trunk to v8.3.herbelin
2010-06-20Test script for bug #1962 (that is apparently solved in 8.3+trunk :-)letouzey
2010-06-18add in test-suite the scripts about fsetdec bugsletouzey
2010-06-16test for bug #2141 (include + extraction)letouzey
2010-06-13Fixing bug 2295 (omission of option "as" in return clause of "match" was notherbelin
2010-06-13Fixing bug 2300 (ltac pattern-matching returning terms with concrete universes).herbelin
2010-06-13Addressed bug #2320 in v8.2 and v8.3 branches ("refine" problem withherbelin
2010-06-12Fixed bug #2135 (second-order unification was raising cryptic message)herbelin
2010-06-12Added regression tests for bugs + miscellaneous improvementsherbelin
2010-06-09Fixed bug # 2303 in r 13087.msozeau
2010-06-09Fix bug #2262: bad implicit argument number by avoiding countingmsozeau
2010-06-09Automatic introduction of names given before ":" in Lemma's andherbelin
2010-05-20Fix bug 2307pboutill
2010-05-10Backporting r13007 (evar_merge wrong and costly) to V8.3 and added test.herbelin
2010-04-29Remove the svn-specific $Id$ annotationsletouzey
2010-04-20Fixed bug #2999 (destruct was not refreshing universes of what it generalized *)herbelin
2010-04-20Propagated fix to bug 2127 (Hint Rewrite badly globalized in modules) to 8.2herbelin
2010-04-10Test for bug #2231 (unexpected error when using let/if over an inductiveherbelin
2010-04-07Granting wish #2251 thanks to commit 12900 solved bug 1416.v (whichherbelin
2010-04-05Granting wish #2251 (forbidding rewriting a term reduced to an evar)herbelin
2010-04-05Tests for bug report #2244 (pattern-unification with abstraction over Meta's)herbelin
2010-03-27Applied greenrd's patch to fix bug 2255 (injection failed toherbelin
2010-02-10bugs/.../1784.v: revert Matthieu's recent fix, since Program has been made co...letouzey
2009-12-30Regression test for bug #2145 (Groebner failing with "not eq" hypotheses).herbelin
2009-12-30Fixing bug #2193: computation of dependencies in the "match" returnherbelin
2009-11-13Fix test-suite scripts: [Generalizable Variables] and small msozeau
2009-09-17Delete trailing whitespaces in all *.{v,ml*} filesglondu
2009-08-13Death of "survive_module" and "survive_section" (the first one washerbelin
2009-07-15- Granted wish #2138 (support for local binders in syntax of Record fields).herbelin
2009-07-08Reactivation of pattern unification of evars in apply unification, inherbelin
2009-04-20Fix wrong pattern in Morphisms. Fix bug scripts to reflect the fact thatmsozeau
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-16 14:12:05 +0000