aboutsummaryrefslogtreecommitdiff
path: root/test-suite
AgeCommit message (Expand)Author
2010-06-04Backported r13068 to branch v8.3 (whd_betaiota on inferred returnherbelin
2010-06-04Grobner.v removedpottier
2010-06-03plugin groebner updated and renamed as nsatz; first version of the doc of nsa...pottier
2010-06-02Fix xml test in non-local modeglondu
2010-06-02Fix test-suite cleaningglondu
2010-05-31Introducing strong typing for IDE - toplevel IPCvgross
2010-05-28A little bit of cleanup, and some annotations.fkirchne
2010-05-20Added examples for checking that the guard condition excludes subtermsherbelin
2010-05-20Fix bug 2307pboutill
2010-05-20fixed guard check with commutative cutsbarras
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-26Disable ideal-features tests by defaultglondu
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-19Reduced the complexity of evar instantiations from O(n^3) to less than O(n^2).herbelin
2010-04-18Fixed some printing bugs.herbelin
2010-04-17Moved Case3.v from ideal features to success (it works since 8.2).herbelin
2010-04-13Remove only *.v.log files in clean of test-suite/Makefileglondu
2010-04-11Recovering 8.2 behavior of "simple (e)apply" (and hence of "(e)auto").herbelin
2010-04-10Prettier test-suite/Makefileglondu
2010-04-10Optimized need for delimiters when disjoint scopes for strings andherbelin
2010-04-10Use the Makefile in test-suite/checkglondu
2010-04-10Makefile for the test-suiteglondu
2010-04-10Fix typos in test-suite scriptglondu
2010-04-10Test for bug #2231 (unexpected error when using let/if over an inductiveherbelin
2010-04-07Commit 12906 continued (forgotten file).herbelin
2010-04-07Granting wish #2251 thanks to commit 12900 solved bug 1416.v (whichherbelin
2010-04-06New model for user-driven translation of tokens in coqdocherbelin
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-30Small things about coqdoc + fixing lettuple.v test (part of bug #2289)herbelin
2010-03-29Several bug-fixes and improvements of coqdocherbelin
2010-03-27Fixing bug #2279 (printing nested let-in was in exponential time)herbelin
2010-03-27Applied greenrd's patch to fix bug 2255 (injection failed toherbelin
2010-03-24Fixed bug #2260 (check of resolution of all evars in the declarationherbelin
2010-03-23Added automatic expansion on the left of recursive notationsherbelin
2010-03-23Fix bug in backtracking.vgross
2010-03-12fixed minor pbs with test casesbarras
2010-03-12fixed confusion between number of cstr arguments and number of pattern variab...barras
2010-03-11introduced lazy computation of size info in the guard conditionbarras
2010-03-11Minimal test suite for search commandspuech
2010-02-26New backtracking code + fix bug #2082.vgross
2010-02-13Fix NumbersSyntax.outletouzey
2010-02-10ajout test de fied_simplify_eq inbarras
2010-02-10bugs/.../1784.v: revert Matthieu's recent fix, since Program has been made co...letouzey
2010-01-29minor change in test-suite/output/NumberSyntax.out: a BigN.t_ instead of BigN.tletouzey
2010-01-12New version of 12650 that was broken (supporting again records whenherbelin
2010-01-12revert commit 12650 for the moment, since it breaks MSetAVLletouzey
2010-01-12Temporary fix to compensate the loss of descent on dependentherbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-13 19:56:46 +0000