aboutsummaryrefslogtreecommitdiff
path: root/test-suite
AgeCommit message (Expand)Author
2010-02-26New backtracking code + fix bug #2082.vgross
2010-02-13Fix NumbersSyntax.outletouzey
2010-02-10ajout test de fied_simplify_eq inbarras
2010-02-10bugs/.../1784.v: revert Matthieu's recent fix, since Program has been made co...letouzey
2010-01-29minor change in test-suite/output/NumberSyntax.out: a BigN.t_ instead of BigN.tletouzey
2010-01-12New version of 12650 that was broken (supporting again records whenherbelin
2010-01-12revert commit 12650 for the moment, since it breaks MSetAVLletouzey
2010-01-12Temporary fix to compensate the loss of descent on dependentherbelin
2010-01-04Errors issued by reduction tactics (e.g. pattern) were not caught by "try".herbelin
2009-12-30Regression test for bug #2145 (Groebner failing with "not eq" hypotheses).herbelin
2009-12-30Fixing bug #2193: computation of dependencies in the "match" returnherbelin
2009-12-30Fixing bug #2146 (broken selection of occurrences in "change").herbelin
2009-12-29Renouncing to have the option "Automatic Introduction" on by default.herbelin
2009-12-29Improving descend_in_conjunctions (using a combinators instead of a tactic)herbelin
2009-12-24In "simpl c" and "change c with d", c can be a pattern.herbelin
2009-12-13Made the side-conditions of lemmas always come last when chaining "apply in"herbelin
2009-12-13Revision 12557 continued (better rendering of dependent rewrite)herbelin
2009-12-03Still continuing r12485-12486, r12549, r12556 (cleaning around name generation)herbelin
2009-12-02Continuing r12485-12486 and r12549 (cleaning around name generation)herbelin
2009-12-02Remove interface pluginglondu
2009-12-01Continuing r12485-12486 (cleaning around name generation)herbelin
2009-11-30Fix backtracking heuristic in typeclass resolution. msozeau
2009-11-27Added support for definition of fixpoints using tactics.herbelin
2009-11-27Substitute terms for evars-as-goals as soon as they are solved inmsozeau
2009-11-26Fixing xml theory file export (was not consistent with coqdoc fileherbelin
2009-11-13Fix test-suite scripts: [Generalizable Variables] and small msozeau
2009-11-12Restore test-suite/csdp.cache erased from svn by mistakeletouzey
2009-11-12BigQ / BigN / BigZ syntax and scope improvements (sequel to 12504)letouzey
2009-11-12Repair interpretation of numeral for BigQ, add a printer (close #2160)letouzey
2009-11-11Redoing broken commit r12498 (fixing bug #2167 + attempt to test theherbelin
2009-11-11Fixing bug #2167 + attempt to test the compatibility of a more robustherbelin
2009-11-11Test for bug #2168, forgotten in r12496.herbelin
2009-11-11Fixed bug #2168 (closing a section may have as side-effect the erasureherbelin
2009-11-11Improving abbreviations/notations + backtrack of semantic change in r12439herbelin
2009-11-09git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12483 85f007b7-540e-0...fbesson
2009-11-08Restructuration of command.ml + generic infrastructure for inductive schemesherbelin
2009-10-30Attempt to capture on time unification errors for "with" bindings.herbelin
2009-10-29Revision 12439 continued, printing part (notations to names behaveherbelin
2009-10-28Integrate a few improvements on typeclasses and Program from the equations br...msozeau
2009-10-28Made that notations to names behave like the names they refer to wrtherbelin
2009-10-26Local/Global revision 12418 continuedherbelin
2009-10-26Adapted test unfold.v after eq gets its argument maximally insertedherbelin
2009-10-25Restore (and test) broken chaining of lemmas in "apply in" in presenceherbelin
2009-10-25Add support for remaining side-conditions in "apply in as".herbelin
2009-10-25Improved the treatment of Local/Global options (noneffective Local onherbelin
2009-10-17Fixed a notation bug when extending binder_constr with empty levelsherbelin
2009-10-08Fixed a bug introduced in revision 12265.herbelin
2009-10-04Removal of trailing spaces.serpyc
2009-09-27Fixed a bug in the interaction between dEqThen and inject_at_positionsherbelin
2009-09-27Fixed two tests that was incorrectly typed in former revisions 12348 and 12356.herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 08:00:01 +0000