aboutsummaryrefslogtreecommitdiff
path: root/test-suite/success
AgeCommit message (Expand)Author
2010-07-28unification des tactiques nsatz pour R Z avec celle des anneaux integrespottier
2010-07-27nstaz pour les anneaux integres et les setoides, R Z et Qpottier
2010-07-24Updated all headers for 8.3 and trunkherbelin
2010-07-12Fix compilation and test-suite of nsatzglondu
2010-07-08nsatz in an integral domain with specialization to Z and Rpottier
2010-06-29Made tclABSTRACT normalize evars before saying it does not supportherbelin
2010-06-25Restored a "feature" of unification in pre-8.3 (it was used e.g. in aherbelin
2010-06-13Fixed bug #2314 (inversion using not checking the correctness of its argumentsherbelin
2010-06-11Mainly made that evarconv is able to solve "?n = (fun x => x) ?n" (sic).herbelin
2010-06-09Automatic introduction of names given before ":" in Lemma's andherbelin
2010-06-09Backported r13080 (support for open terms in ltac matching) from trunk to v8.3.herbelin
2010-06-06Added support for Ltac-matching terms with variables bound in the patternherbelin
2010-06-04Grobner.v removedpottier
2010-06-03plugin groebner updated and renamed as nsatz; first version of the doc of nsa...pottier
2010-04-29Remove the svn-specific $Id$ annotationsletouzey
2010-04-17Moved Case3.v from ideal features to success (it works since 8.2).herbelin
2010-04-11Recovering 8.2 behavior of "simple (e)apply" (and hence of "(e)auto").herbelin
2010-04-07Commit 12906 continued (forgotten file).herbelin
2010-03-23Added automatic expansion on the left of recursive notationsherbelin
2010-03-12fixed minor pbs with test casesbarras
2010-03-12fixed confusion between number of cstr arguments and number of pattern variab...barras
2010-02-10ajout test de fied_simplify_eq inbarras
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-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-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-13Fix test-suite scripts: [Generalizable Variables] and small msozeau
2009-11-11Test for bug #2168, forgotten in r12496.herbelin
2009-11-11Improving abbreviations/notations + backtrack of semantic change in r12439herbelin
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-04Removal of trailing spaces.serpyc
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-24 16:58:52 +0000