aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite
Commit message (Expand)AuthorAge
* Fix inconsistency in Prop/Set conversion checkGravatar glondu2010-09-23
* Fixed test of bug #2360 (use of Fail to check a regular error insteadGravatar herbelin2010-09-20
* Fixing bug #2360 (descend_in_conjunctions built ill-typed terms). Shouldn't weGravatar herbelin2010-09-19
* Added test for bugs 2242, 2337, 2339 + remove the use of name "ambiguous" inGravatar herbelin2010-09-18
* Fixing bugs #2347 (part 2) and #2388: error message printing was doneGravatar herbelin2010-09-18
* Fixed a problem introduced in r12607 after pattern_of_constr servedGravatar herbelin2010-09-17
* In the computation of missing arguments for apply, accept that theGravatar herbelin2010-09-17
* Improving a few error messages in Ltac interpretationGravatar herbelin2010-09-11
* fixed bug #2375 (congruence)Gravatar corbinea2010-09-02
* Updated test on Nsatz after Loïc moved NsatzR to Nsatz.Gravatar herbelin2010-07-30
* test-case for bug #2105Gravatar barras2010-07-29
* unification des tactiques nsatz pour R Z avec celle des anneaux integresGravatar pottier2010-07-28
* fixed bug #2139: compiled cofix loops, missing offset to evaluate cofix bodiesGravatar barras2010-07-28
* nstaz pour les anneaux integres et les setoides, R Z et QGravatar pottier2010-07-27
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-11 10:46:43 +0000