aboutsummaryrefslogtreecommitdiff
path: root/test-suite/bugs
AgeCommit message (Expand)Author
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-13Addressed bug #2310 and replaced anomaly "unknown meta" raised by "refine"herbelin
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
2009-04-16Fix bug #2089: correctly dealing with parameters and real arguments inmsozeau
2009-04-14Fix and actually beautify the bug script to adapt to the new measuremsozeau
2009-03-29Avoid inadvertent declaration of "on" as a keyword. New syntax ismsozeau
2009-03-26Fixes in Program well-founded definitions:msozeau
2009-01-20Fixing bug #1918 (no occur-check in Meta unification was done yet!).herbelin
2009-01-20- Fixing bug 1891 (abusive instantiations of evar arguments inherbelin
2009-01-18Backporting from v8.2 to trunk:herbelin
2009-01-12Fix a bunch of bugs related to setoid_rewrite, unification and evars:msozeau
2009-01-11- Deactivation of dynamic loading on Mac OS 10.5 (see bug #2024).herbelin
2009-01-04Fixed bugs #2001 (search_guard was overwriting the guard index givenherbelin
2009-01-01- Fixed bug #2021 (uncaught exception with injection/discriminate whenherbelin
2008-12-16Finish fix for the treatment of [inverse] in [setoid_rewrite], making amsozeau
2008-11-27fixed bug 1791: simpl was performing eta expansionbarras
2008-11-26closed bug 1898: fold x in x; added a reordering primitive tacticbarras
2008-11-23Fixed bug #2006 (type constraint on Record was not taken into account) +herbelin
2008-11-14Add missing test-suite files for closed bugs.msozeau
2008-11-13git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11583 85f007b7-540e-0...barras
2008-09-16Report change of the implicit argument status of the carrier type in themsozeau
2008-09-14Fix bug #1931 by searching for a sort after doing beta,iota,delta-msozeau
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-07 06:18:27 +0000