aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite
Commit message (Expand)AuthorAge
* Notations are back in the "in" clause of pattern matching.Gravatar pboutill2012-05-15
* Implicit arguments of Definition are taken from the type when given by the user.Gravatar pboutill2012-04-27
* remove undocumented and scarcely-used tactic auto decompGravatar letouzey2012-04-23
* Bug 2733 : { } implicits and FixpointsGravatar pboutill2012-04-17
* Fixing tauto "special" behavior on singleton types w/ 2 parameters (bug #2680).Gravatar herbelin2012-04-15
* Repair two testsGravatar letouzey2012-04-12
* Fixing a few bugs (see #2571) related to interpretation of multiple bindersGravatar herbelin2012-04-06
* Relax uniform inheritance conditionGravatar gareuselesinge2012-04-05
* Unification: Added a heuristic to solve problems of the formGravatar herbelin2012-03-26
* Fix the test-suite by removing any Reset in the scriptsGravatar letouzey2012-03-23
* evarconv: MaybeFlex/MaybeFlex case infers more Canonical StructuresGravatar gareuselesinge2012-03-22
* Fixing bug #2724 (using notations with binders in cases patternsGravatar herbelin2012-03-20
* Fixing alpha-conversion bug #2723 introduced in r12485-12486.Gravatar herbelin2012-03-20
* Generalized the use of evar candidates in type inference unification:Gravatar herbelin2012-03-20
* Fix bugs related to Program integration.Gravatar msozeau2012-03-19
* Fixing bug #2732 (anomaly when using the tolerance for writingGravatar herbelin2012-03-18
* Fixing vm_compute bug #2729 (function used to decompose constructorsGravatar herbelin2012-03-13
* "Let in" in pattern hell, one more iterationGravatar pboutill2012-03-02
* Noise for nothingGravatar pboutill2012-03-02
* Use a heuristic to not simplify equality hypotheses remaining after dependent...Gravatar msozeau2012-02-20
* Arguments supports extra notation scopesGravatar gareuselesinge2012-02-14
* Fix consequence of pp bugfix in testsuiteGravatar pboutill2012-01-31
* Fix simplification of ind. hyps., recognized by a [block] in their type (bug ...Gravatar msozeau2012-01-28
* Notations with binders: Accepting using notations for functional termsGravatar herbelin2012-01-20
* Parameters in pattern first step.Gravatar pboutill2012-01-16
* Add distclean back to test-suite/MakefileGravatar glondu2012-01-14
* Backtracking on r14876 (fix for bug #2267): extra scopes might beGravatar herbelin2012-01-05
* Fixing Arguments Scope bug when too many scopes are given (bug #2667).Gravatar herbelin2012-01-04
* Type inference unification: fixed a 8.4 bug in the presence of unificationGravatar herbelin2012-01-04
* Arguments: check rename even if no implicit is specifiedGravatar gareuselesinge2011-12-19
* test suite update after r14808Gravatar pboutill2011-12-19
* Fixing bug #2634 (unscoped notations were disturbing theGravatar herbelin2011-12-18
* Fixed a Not_found bug when declaring in a section some implicitGravatar herbelin2011-12-18
* Added ability to take the type of applied metas into account whenGravatar herbelin2011-12-17
* Command Arguments: standardizing format of error messages and American spelling.Gravatar herbelin2011-12-17
* Bypassing the use of (currently unimplemented) "Show Script" in testsGravatar herbelin2011-12-17
* Fixing format of complexity bug Notations.v.Gravatar herbelin2011-12-17
* Fixing amazing loop when using eta-expansion in pattern-matching forGravatar herbelin2011-12-16
* Proof using ...Gravatar gareuselesinge2011-12-12
* Fixing grammar resetting bug in the presence of levels initially emptyGravatar herbelin2011-12-07
* Adapting test Existentials to new numbering strategy of evars (r14764).Gravatar herbelin2011-12-07
* Fixing a bug of commit r13310 (activating coercions only when moduleGravatar herbelin2011-12-07
* Minor fixes to ArgumentsGravatar gareuselesinge2011-12-06
* A small test for type inference (used to be a regression at some time).Gravatar herbelin2011-12-04
* Fixing superflous newline in output of About when no parameter is renamed.Gravatar herbelin2011-12-04
* Discarding let-ins from the instances of the evars in theGravatar herbelin2011-12-04
* Quick hack to avoid anomaly on using Program w/o having required JMeq.Gravatar herbelin2011-11-30
* Extraction: Richer patterns in matchs as proposed by P.N. TollitteGravatar letouzey2011-11-28
* Fixed a bug in postprocessing dependencies in pattern-matching compilationGravatar herbelin2011-11-26
* Renamig support added to "Arguments"Gravatar gareuselesinge2011-11-21