aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite
Commit message (Expand)AuthorAge
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
* Extension of the recursive notations mechanismGravatar herbelin2010-07-22
* Backporting fix to bug #2353 (fixpoint with recursively non-uniformGravatar herbelin2010-07-21
* Quick fix for bug #2350 (ensuring enough "red" when refine calls fix tactic).Gravatar herbelin2010-07-21
* Fix compilation and test-suite of nsatzGravatar glondu2010-07-12
* nsatz in an integral domain with specialization to Z and RGravatar pottier2010-07-08
* Fix (part of) bug #2347, de Bruijn bug in Program's pretyper.Gravatar msozeau2010-06-30
* Made tclABSTRACT normalize evars before saying it does not supportGravatar herbelin2010-06-29
* Backporting modifications to nsatz (doc + fix of bug #2328) from trunk to v8.3.Gravatar herbelin2010-06-26
* Restored a "feature" of unification in pre-8.3 (it was used e.g. in aGravatar herbelin2010-06-25
* Test script for bug #1962 (that is apparently solved in 8.3+trunk :-)Gravatar letouzey2010-06-20
* Hack for fixing bug #2172 (see explanations in file rewrite-2172.v).Gravatar herbelin2010-06-18
* add in test-suite the scripts about fsetdec bugsGravatar letouzey2010-06-18
* test for bug #2141 (include + extraction)Gravatar letouzey2010-06-16
* Added printing of recursive notations in cases pattern (supported by wish 2248).Gravatar herbelin2010-06-14
* Fixing bug 2295 (omission of option "as" in return clause of "match" was notGravatar herbelin2010-06-13
* Fixing bug 2300 (ltac pattern-matching returning terms with concrete universes).Gravatar herbelin2010-06-13
* Addressed bug #2320 in v8.2 and v8.3 branches ("refine" problem withGravatar herbelin2010-06-13
* Addressed bug #2310 and replaced anomaly "unknown meta" raised by "refine"Gravatar herbelin2010-06-13
* Fixed bug #2314 (inversion using not checking the correctness of its argumentsGravatar herbelin2010-06-13
* Fixed bug #2135 (second-order unification was raising cryptic message)Gravatar herbelin2010-06-12
* Added regression tests for bugs + miscellaneous improvementsGravatar herbelin2010-06-12
* Mainly made that evarconv is able to solve "?n = (fun x => x) ?n" (sic).Gravatar herbelin2010-06-11
* Fixed bug # 2303 in r 13087.Gravatar msozeau2010-06-09
* Fix bug #2262: bad implicit argument number by avoiding countingGravatar msozeau2010-06-09
* Automatic introduction of names given before ":" in Lemma's andGravatar herbelin2010-06-09
* Backported r13080 (support for open terms in ltac matching) from trunk to v8.3.Gravatar herbelin2010-06-09
* Added support for Ltac-matching terms with variables bound in the patternGravatar herbelin2010-06-06
* Backported r13068 to branch v8.3 (whd_betaiota on inferred returnGravatar herbelin2010-06-04
* Grobner.v removedGravatar pottier2010-06-04
* plugin groebner updated and renamed as nsatz; first version of the doc of nsa...Gravatar pottier2010-06-03
* Fix xml test in non-local modeGravatar glondu2010-06-02
* Fix test-suite cleaningGravatar glondu2010-06-02
* Introducing strong typing for IDE - toplevel IPCGravatar vgross2010-05-31
* A little bit of cleanup, and some annotations.Gravatar fkirchne2010-05-28
* Added examples for checking that the guard condition excludes subtermsGravatar herbelin2010-05-20
* Fix bug 2307Gravatar pboutill2010-05-20
* fixed guard check with commutative cutsGravatar barras2010-05-20
* Backporting r13007 (evar_merge wrong and costly) to V8.3 and added test.Gravatar herbelin2010-05-10
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
* Disable ideal-features tests by defaultGravatar glondu2010-04-26
* Fixed bug #2999 (destruct was not refreshing universes of what it generalized *)Gravatar herbelin2010-04-20
* Propagated fix to bug 2127 (Hint Rewrite badly globalized in modules) to 8.2Gravatar herbelin2010-04-20
* Reduced the complexity of evar instantiations from O(n^3) to less than O(n^2).Gravatar herbelin2010-04-19
* Fixed some printing bugs.Gravatar herbelin2010-04-18
* Moved Case3.v from ideal features to success (it works since 8.2).Gravatar herbelin2010-04-17
* Remove only *.v.log files in clean of test-suite/MakefileGravatar glondu2010-04-13
* Recovering 8.2 behavior of "simple (e)apply" (and hence of "(e)auto").Gravatar herbelin2010-04-11
* Prettier test-suite/MakefileGravatar glondu2010-04-10
* Optimized need for delimiters when disjoint scopes for strings andGravatar herbelin2010-04-10
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-06 00:48:53 +0000