aboutsummaryrefslogtreecommitdiff
path: root/test-suite/bugs
AgeCommit message (Expand)Author
2012-06-20Fixing bug #2817 (occur check was not done up to instantiation ofherbelin
2012-04-27Implicit arguments of Definition are taken from the type when given by the user.pboutill
2012-04-17Bug 2733 : { } implicits and Fixpointspboutill
2012-04-15Fixing tauto "special" behavior on singleton types w/ 2 parameters (bug #2680).herbelin
2012-04-12Repair two testsletouzey
2012-03-20Generalized the use of evar candidates in type inference unification:herbelin
2012-03-19Fix bugs related to Program integration.msozeau
2012-03-18Fixing bug #2732 (anomaly when using the tolerance for writingherbelin
2012-03-13Fixing vm_compute bug #2729 (function used to decompose constructorsherbelin
2012-01-05Backtracking on r14876 (fix for bug #2267): extra scopes might beherbelin
2012-01-04Fixing Arguments Scope bug when too many scopes are given (bug #2667).herbelin
2011-11-21Extend the computation of dependencies in pattern-matching compilationherbelin
2011-11-17Fixing bug #2640 and variants of it (inconsistency between when andherbelin
2011-11-16Fixing bug #1834 (de Bruijn indices bug in pattern-matching compilation).herbelin
2011-10-25Regression tests for bugs #2613 and #2616.herbelin
2011-10-25New strategy to infer return predicate of match construct whenherbelin
2011-10-24Mod_subst: Attempt to fix #2608letouzey
2011-10-18Fix bug #2473 due to wrong folding of the evar environmentmsozeau
2011-10-18Fix inductive coercion code in Program (bug #2378)msozeau
2011-10-18Fix bug #2586 and enhance clsubst* as well as a side effectmsozeau
2011-10-17Fix bug #2456 and wrong unfolding of lets in the goal due to [unfold] doing z...msozeau
2011-10-12test-suite: non-regression test for bug #2603letouzey
2011-10-11Added test for bug #2615herbelin
2011-10-07fsetdec : non-atomic elements are now transformed as variables first (fix #2464)letouzey
2011-10-07Improved handling of element equalities in fsetdec (fix #2467)letouzey
2011-09-15Omega aware of Z.pred (fix #1912)letouzey
2011-09-15Re-allowing assumptions during proofs seems safe now (fix #2411)letouzey
2011-06-18Relaxed the constraint introduced in r14190 that froze the existingherbelin
2011-06-18r14204 and 14218 continued: completely removing test for bug #2490,herbelin
2011-06-18Partial backtrack on wrong r14204: bug #2490 still open.herbelin
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-07 00:53:16 +0000