aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite
Commit message (Expand)AuthorAge
* 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
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
* git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12294 85f007b7-540e-0...Gravatar fbesson2009-08-25
* + csdp.cacheGravatar fbesson2009-08-15
* Death of "survive_module" and "survive_section" (the first one wasGravatar herbelin2009-08-13
* Ensures that let-in's in arities of inductive types work well. Maybe notGravatar herbelin2009-08-11
* Relatively ad hoc fix to an ill-typed instantiation bug in typeGravatar herbelin2009-08-11
* psatz Z -> psatz Z 1Gravatar fbesson2009-07-30
* Remove the barely-used/obsolete/undocumented syntax "conditional <tac> rewrite"Gravatar letouzey2009-07-24
* Move some examples for groebner into a test-suite fileGravatar letouzey2009-07-20
* - Granted wish #2138 (support for local binders in syntax of Record fields).Gravatar herbelin2009-07-15
* Reactivation of pattern unification of evars in apply unification, inGravatar herbelin2009-07-08
* Fixing bug #2106 ("match" compilation with multi-dependent constructor).Gravatar herbelin2009-06-06
* Adding a regression test about Bauer's example on coq-club ofGravatar herbelin2009-06-02
* Fix script file using the "Manual Implicit" flag.Gravatar msozeau2009-06-02
* micromega: proof compression bugfixGravatar fbesson2009-05-11
* - Addition of "Hint Resolve ->" and "Hint Resolve <-" continued: itGravatar herbelin2009-05-10
* - Fixing #2090 (occur check missing when trying to solve evar-evar equation).Gravatar herbelin2009-04-25
* Fix test output mentionning an existential number that changed.Gravatar msozeau2009-04-20
* Fix wrong pattern in Morphisms. Fix bug scripts to reflect the fact thatGravatar msozeau2009-04-20
* Fix bug #2089: correctly dealing with parameters and real arguments inGravatar msozeau2009-04-16
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-02 22:08:44 +0000