aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite
Commit message (Expand)AuthorAge
* Add "Print Sorted Universes"Gravatar glondu2011-01-11
* Fixing an uncaught exception bug with use of vmcastGravatar herbelin2011-01-07
* Remove the two-argument variant of "decide equality"Gravatar glondu2010-12-23
* Extraction: avoid type-unsafe optimisation of pattern-matchings (fix #2413)Gravatar letouzey2010-12-21
* 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
* Fix missing -coqlib argument to coqdep in test-suiteGravatar glondu2010-10-16
* Adding test-case for bug #2362, which uses HO unification duringGravatar msozeau2010-10-12
* Fix bug #2393: allow let-ins inside telescopes (only fails when there'sGravatar msozeau2010-10-12
* Backporting r13521 from branch 8.3 to trunk (fixing bug #2406, loopingGravatar herbelin2010-10-11
* test-suite: fix success/unification.vGravatar glondu2010-10-07
* test-suite: fix output/Existentials.outGravatar glondu2010-10-06
* 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
* test-suite: use unified diff output and use expected output as referenceGravatar glondu2010-10-05
* Fixing bugs in previous commits about implicit arguments:Gravatar herbelin2010-10-04
* Test for non-regression of the display bug fixed in r13486.Gravatar herbelin2010-10-03
* Added multiple implicit arguments rules per name.Gravatar herbelin2010-10-03
* Making display of various informations about constants more modular:Gravatar herbelin2010-10-03
* Improve handling of metas as evars in unification (patch by Hugo)Gravatar letouzey2010-09-30
* Fix inconsistency in Prop/Set conversion checkGravatar glondu2010-09-23
* Fixed test of bug #2360 (use of Fail to check a regular error insteadGravatar herbelin2010-09-20
* Fixing bug #2360 (descend_in_conjunctions built ill-typed terms). Shouldn't weGravatar herbelin2010-09-19
* Added test for bugs 2242, 2337, 2339 + remove the use of name "ambiguous" inGravatar herbelin2010-09-18
* Fixing bugs #2347 (part 2) and #2388: error message printing was doneGravatar herbelin2010-09-18
* 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
* fixed bug #2375 (congruence)Gravatar corbinea2010-09-02
* Updated test on Nsatz after Loïc moved NsatzR to Nsatz.Gravatar herbelin2010-07-30
* test-case for bug #2105Gravatar barras2010-07-29
* unification des tactiques nsatz pour R Z avec celle des anneaux integresGravatar pottier2010-07-28
* fixed bug #2139: compiled cofix loops, missing offset to evaluate cofix bodiesGravatar barras2010-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
* Extension of the recursive notations mechanismGravatar herbelin2010-07-22
* Backporting fix to bug #2353 (fixpoint with recursively non-uniformGravatar herbelin2010-07-21
* Quick fix for bug #2350 (ensuring enough "red" when refine calls fix tactic).Gravatar herbelin2010-07-21
* Fix compilation and test-suite of nsatzGravatar glondu2010-07-12
* nsatz in an integral domain with specialization to Z and RGravatar pottier2010-07-08
* Fix (part of) bug #2347, de Bruijn bug in Program's pretyper.Gravatar msozeau2010-06-30
* Made tclABSTRACT normalize evars before saying it does not supportGravatar herbelin2010-06-29
* Backporting modifications to nsatz (doc + fix of bug #2328) from trunk to v8.3.Gravatar herbelin2010-06-26
* Restored a "feature" of unification in pre-8.3 (it was used e.g. in aGravatar herbelin2010-06-25
* Test script for bug #1962 (that is apparently solved in 8.3+trunk :-)Gravatar letouzey2010-06-20
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-10 17:46:09 +0000