aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/success
Commit message (Expand)AuthorAge
* Remove the two-argument variant of "decide equality"Gravatar glondu2010-12-23
* Fixing bug #2454: inversion predicate strategy for inferring the typeGravatar herbelin2010-12-19
* Fixing bug #2448 (wrongly-scoped alpha-renaming in notations).Gravatar herbelin2010-12-04
* Fixing bug using explictly declared implicit arguments in inductive arities.Gravatar herbelin2010-12-03
* Fixing a bug introduced in r12304 (move of interpretation ofGravatar herbelin2010-12-02
* SearchAbout: who has never been annoyed by the [ ] syntax ?Gravatar letouzey2010-11-19
* An experimental support for open constrs in hints and in "using"Gravatar herbelin2010-10-31
* test-suite: fix success/unification.vGravatar glondu2010-10-07
* test-suite: fix success/Typeclasses.vGravatar glondu2010-10-05
* test-suite: fix success/AdvancedCanonicalStructure.vGravatar glondu2010-10-05
* Export definition of type implicits_list for contribs + fixed aGravatar herbelin2010-10-05
* Fixing bugs in previous commits about implicit arguments:Gravatar herbelin2010-10-04
* Added multiple implicit arguments rules per name.Gravatar herbelin2010-10-03
* Improve handling of metas as evars in unification (patch by Hugo)Gravatar letouzey2010-09-30
* Fixed a problem introduced in r12607 after pattern_of_constr servedGravatar herbelin2010-09-17
* In the computation of missing arguments for apply, accept that theGravatar herbelin2010-09-17
* Improving a few error messages in Ltac interpretationGravatar herbelin2010-09-11
* unification des tactiques nsatz pour R Z avec celle des anneaux integresGravatar pottier2010-07-28
* nstaz pour les anneaux integres et les setoides, R Z et QGravatar pottier2010-07-27
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
* Fix compilation and test-suite of nsatzGravatar glondu2010-07-12
* nsatz in an integral domain with specialization to Z and RGravatar pottier2010-07-08
* Made tclABSTRACT normalize evars before saying it does not supportGravatar herbelin2010-06-29
* Restored a "feature" of unification in pre-8.3 (it was used e.g. in aGravatar herbelin2010-06-25
* Fixed bug #2314 (inversion using not checking the correctness of its argumentsGravatar herbelin2010-06-13
* Mainly made that evarconv is able to solve "?n = (fun x => x) ?n" (sic).Gravatar herbelin2010-06-11
* Automatic introduction of names given before ":" in Lemma's andGravatar herbelin2010-06-09
* Backported r13080 (support for open terms in ltac matching) from trunk to v8.3.Gravatar herbelin2010-06-09
* Added support for Ltac-matching terms with variables bound in the patternGravatar herbelin2010-06-06
* Grobner.v removedGravatar pottier2010-06-04
* plugin groebner updated and renamed as nsatz; first version of the doc of nsa...Gravatar pottier2010-06-03
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
* Moved Case3.v from ideal features to success (it works since 8.2).Gravatar herbelin2010-04-17
* Recovering 8.2 behavior of "simple (e)apply" (and hence of "(e)auto").Gravatar herbelin2010-04-11
* Commit 12906 continued (forgotten file).Gravatar herbelin2010-04-07
* Added automatic expansion on the left of recursive notationsGravatar herbelin2010-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
* ajout test de fied_simplify_eq inGravatar barras2010-02-10
* 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
* 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
* Fix backtracking heuristic in typeclass resolution. Gravatar msozeau2009-11-30
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-01 08:51:10 +0000