aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite
Commit message (Expand)AuthorAge
* 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
* Local/Global revision 12418 continuedGravatar herbelin2009-10-26
* Adapted test unfold.v after eq gets its argument maximally insertedGravatar herbelin2009-10-26
* Restore (and test) broken chaining of lemmas in "apply in" in presenceGravatar herbelin2009-10-25
* Add support for remaining side-conditions in "apply in as".Gravatar herbelin2009-10-25
* Improved the treatment of Local/Global options (noneffective Local onGravatar herbelin2009-10-25
* Fixed a notation bug when extending binder_constr with empty levelsGravatar herbelin2009-10-17
* Fixed a bug introduced in revision 12265.Gravatar herbelin2009-10-08
* Removal of trailing spaces.Gravatar serpyc2009-10-04
* Fixed a bug in the interaction between dEqThen and inject_at_positionsGravatar herbelin2009-09-27
* Fixed two tests that was incorrectly typed in former revisions 12348 and 12356.Gravatar herbelin2009-09-27
* Delay the choice of eliminator in destruct/induction until we know ifGravatar herbelin2009-09-27
* Micromega doc : psatz Z -> psatz Z 2Gravatar fbesson2009-09-24
* Add the option to automatically introduce variables declared before theGravatar msozeau2009-09-22
* Only one "in" clause in "destruct" even for a multiple "destruct".Gravatar herbelin2009-09-20
* micromega: better handling of exponentiation + correction of test-suite termi...Gravatar fbesson2009-09-18
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-03 01:40:18 +0000