aboutsummaryrefslogtreecommitdiff
path: root/test-suite
AgeCommit message (Expand)Author
2012-05-15Notations are back in the "in" clause of pattern matching.pboutill
2012-04-27Implicit arguments of Definition are taken from the type when given by the user.pboutill
2012-04-23remove undocumented and scarcely-used tactic auto decompletouzey
2012-04-17Bug 2733 : { } implicits and Fixpointspboutill
2012-04-15Fixing tauto "special" behavior on singleton types w/ 2 parameters (bug #2680).herbelin
2012-04-12Repair two testsletouzey
2012-04-06Fixing a few bugs (see #2571) related to interpretation of multiple bindersherbelin
2012-04-05Relax uniform inheritance conditiongareuselesinge
2012-03-26Unification: Added a heuristic to solve problems of the formherbelin
2012-03-23Fix the test-suite by removing any Reset in the scriptsletouzey
2012-03-22evarconv: MaybeFlex/MaybeFlex case infers more Canonical Structuresgareuselesinge
2012-03-20Fixing bug #2724 (using notations with binders in cases patternsherbelin
2012-03-20Fixing alpha-conversion bug #2723 introduced in r12485-12486.herbelin
2012-03-20Generalized the use of evar candidates in type inference unification:herbelin
2012-03-19Fix bugs related to Program integration.msozeau
2012-03-18Fixing bug #2732 (anomaly when using the tolerance for writingherbelin
2012-03-13Fixing vm_compute bug #2729 (function used to decompose constructorsherbelin
2012-03-02"Let in" in pattern hell, one more iterationpboutill
2012-03-02Noise for nothingpboutill
2012-02-20Use a heuristic to not simplify equality hypotheses remaining after dependent...msozeau
2012-02-14Arguments supports extra notation scopesgareuselesinge
2012-01-31Fix consequence of pp bugfix in testsuitepboutill
2012-01-28Fix simplification of ind. hyps., recognized by a [block] in their type (bug ...msozeau
2012-01-20Notations with binders: Accepting using notations for functional termsherbelin
2012-01-16Parameters in pattern first step.pboutill
2012-01-14Add distclean back to test-suite/Makefileglondu
2012-01-05Backtracking on r14876 (fix for bug #2267): extra scopes might beherbelin
2012-01-04Fixing Arguments Scope bug when too many scopes are given (bug #2667).herbelin
2012-01-04Type inference unification: fixed a 8.4 bug in the presence of unificationherbelin
2011-12-19Arguments: check rename even if no implicit is specifiedgareuselesinge
2011-12-19test suite update after r14808pboutill
2011-12-18Fixing bug #2634 (unscoped notations were disturbing theherbelin
2011-12-18Fixed a Not_found bug when declaring in a section some implicitherbelin
2011-12-17Added ability to take the type of applied metas into account whenherbelin
2011-12-17Command Arguments: standardizing format of error messages and American spelling.herbelin
2011-12-17Bypassing the use of (currently unimplemented) "Show Script" in testsherbelin
2011-12-17Fixing format of complexity bug Notations.v.herbelin
2011-12-16Fixing amazing loop when using eta-expansion in pattern-matching forherbelin
2011-12-12Proof using ...gareuselesinge
2011-12-07Fixing grammar resetting bug in the presence of levels initially emptyherbelin
2011-12-07Adapting test Existentials to new numbering strategy of evars (r14764).herbelin
2011-12-07Fixing a bug of commit r13310 (activating coercions only when moduleherbelin
2011-12-06Minor fixes to Argumentsgareuselesinge
2011-12-04A small test for type inference (used to be a regression at some time).herbelin
2011-12-04Fixing superflous newline in output of About when no parameter is renamed.herbelin
2011-12-04Discarding let-ins from the instances of the evars in theherbelin
2011-11-30Quick hack to avoid anomaly on using Program w/o having required JMeq.herbelin
2011-11-28Extraction: Richer patterns in matchs as proposed by P.N. Tollitteletouzey
2011-11-26Fixed a bug in postprocessing dependencies in pattern-matching compilationherbelin
2011-11-21Renamig support added to "Arguments"gareuselesinge
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-01 21:08:58 +0000