aboutsummaryrefslogtreecommitdiff
path: root/test-suite
AgeCommit message (Expand)Author
2010-06-25Restored a "feature" of unification in pre-8.3 (it was used e.g. in aherbelin
2010-06-20Test script for bug #1962 (that is apparently solved in 8.3+trunk :-)letouzey
2010-06-18Hack for fixing bug #2172 (see explanations in file rewrite-2172.v).herbelin
2010-06-18add in test-suite the scripts about fsetdec bugsletouzey
2010-06-16test for bug #2141 (include + extraction)letouzey
2010-06-14Added printing of recursive notations in cases pattern (supported by wish 2248).herbelin
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-13Fixed bug #2314 (inversion using not checking the correctness of its argumentsherbelin
2010-06-12Fixed bug #2135 (second-order unification was raising cryptic message)herbelin
2010-06-12Added regression tests for bugs + miscellaneous improvementsherbelin
2010-06-11Mainly made that evarconv is able to solve "?n = (fun x => x) ?n" (sic).herbelin
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-06-09Backported r13080 (support for open terms in ltac matching) from trunk to v8.3.herbelin
2010-06-06Added support for Ltac-matching terms with variables bound in the patternherbelin
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-01 18:04:55 +0000