aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite
Commit message (Expand)AuthorAge
* 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
* Remove interface pluginGravatar glondu2009-12-02
* Continuing r12485-12486 (cleaning around name generation)Gravatar herbelin2009-12-01
* Fix backtracking heuristic in typeclass resolution. Gravatar msozeau2009-11-30
* Added support for definition of fixpoints using tactics.Gravatar herbelin2009-11-27
* Substitute terms for evars-as-goals as soon as they are solved inGravatar msozeau2009-11-27
* Fixing xml theory file export (was not consistent with coqdoc fileGravatar herbelin2009-11-26
* Fix test-suite scripts: [Generalizable Variables] and small Gravatar msozeau2009-11-13
* Restore test-suite/csdp.cache erased from svn by mistakeGravatar letouzey2009-11-12
* BigQ / BigN / BigZ syntax and scope improvements (sequel to 12504)Gravatar letouzey2009-11-12
* Repair interpretation of numeral for BigQ, add a printer (close #2160)Gravatar letouzey2009-11-12
* Redoing broken commit r12498 (fixing bug #2167 + attempt to test theGravatar herbelin2009-11-11
* Fixing bug #2167 + attempt to test the compatibility of a more robustGravatar herbelin2009-11-11
* Test for bug #2168, forgotten in r12496.Gravatar herbelin2009-11-11
* Fixed bug #2168 (closing a section may have as side-effect the erasureGravatar herbelin2009-11-11
* Improving abbreviations/notations + backtrack of semantic change in r12439Gravatar herbelin2009-11-11
* git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12483 85f007b7-540e-0...Gravatar fbesson2009-11-09
* Restructuration of command.ml + generic infrastructure for inductive schemesGravatar herbelin2009-11-08
* Attempt to capture on time unification errors for "with" bindings.Gravatar herbelin2009-10-30
* Revision 12439 continued, printing part (notations to names behaveGravatar herbelin2009-10-29
* Integrate a few improvements on typeclasses and Program from the equations br...Gravatar msozeau2009-10-28
* Made that notations to names behave like the names they refer to wrtGravatar herbelin2009-10-28
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-11 22:08:20 +0000