aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite
Commit message (Expand)AuthorAge
* 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
* Use the Makefile in test-suite/checkGravatar glondu2010-04-10
* Makefile for the test-suiteGravatar glondu2010-04-10
* Fix typos in test-suite scriptGravatar glondu2010-04-10
* Test for bug #2231 (unexpected error when using let/if over an inductiveGravatar herbelin2010-04-10
* Commit 12906 continued (forgotten file).Gravatar herbelin2010-04-07
* Granting wish #2251 thanks to commit 12900 solved bug 1416.v (whichGravatar herbelin2010-04-07
* New model for user-driven translation of tokens in coqdocGravatar herbelin2010-04-06
* Granting wish #2251 (forbidding rewriting a term reduced to an evar)Gravatar herbelin2010-04-05
* Tests for bug report #2244 (pattern-unification with abstraction over Meta's)Gravatar herbelin2010-04-05
* Small things about coqdoc + fixing lettuple.v test (part of bug #2289)Gravatar herbelin2010-03-30
* Several bug-fixes and improvements of coqdocGravatar herbelin2010-03-29
* Fixing bug #2279 (printing nested let-in was in exponential time)Gravatar herbelin2010-03-27
* Applied greenrd's patch to fix bug 2255 (injection failed toGravatar herbelin2010-03-27
* Fixed bug #2260 (check of resolution of all evars in the declarationGravatar herbelin2010-03-24
* Added automatic expansion on the left of recursive notationsGravatar herbelin2010-03-23
* Fix bug in backtracking.Gravatar vgross2010-03-23
* fixed minor pbs with test casesGravatar barras2010-03-12
* fixed confusion between number of cstr arguments and number of pattern variab...Gravatar barras2010-03-12
* introduced lazy computation of size info in the guard conditionGravatar barras2010-03-11
* Minimal test suite for search commandsGravatar puech2010-03-11
* New backtracking code + fix bug #2082.Gravatar vgross2010-02-26
* Fix NumbersSyntax.outGravatar letouzey2010-02-13
* ajout test de fied_simplify_eq inGravatar barras2010-02-10
* bugs/.../1784.v: revert Matthieu's recent fix, since Program has been made co...Gravatar letouzey2010-02-10
* minor change in test-suite/output/NumberSyntax.out: a BigN.t_ instead of BigN.tGravatar letouzey2010-01-29
* New version of 12650 that was broken (supporting again records whenGravatar herbelin2010-01-12
* revert commit 12650 for the moment, since it breaks MSetAVLGravatar letouzey2010-01-12
* Temporary fix to compensate the loss of descent on dependentGravatar herbelin2010-01-12
* Errors issued by reduction tactics (e.g. pattern) were not caught by "try".Gravatar herbelin2010-01-04
* Regression test for bug #2145 (Groebner failing with "not eq" hypotheses).Gravatar herbelin2009-12-30
* Fixing bug #2193: computation of dependencies in the "match" returnGravatar herbelin2009-12-30
* Fixing bug #2146 (broken selection of occurrences in "change").Gravatar herbelin2009-12-30
* Renouncing to have the option "Automatic Introduction" on by default.Gravatar herbelin2009-12-29
* Improving descend_in_conjunctions (using a combinators instead of a tactic)Gravatar herbelin2009-12-29
* In "simpl c" and "change c with d", c can be a pattern.Gravatar herbelin2009-12-24
* Made the side-conditions of lemmas always come last when chaining "apply in"Gravatar herbelin2009-12-13
* Revision 12557 continued (better rendering of dependent rewrite)Gravatar herbelin2009-12-13
* Still continuing r12485-12486, r12549, r12556 (cleaning around name generation)Gravatar herbelin2009-12-03
* Continuing r12485-12486 and r12549 (cleaning around name generation)Gravatar herbelin2009-12-02
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-01 02:13:35 +0000