aboutsummaryrefslogtreecommitdiff
path: root/test-suite
AgeCommit message (Expand)Author
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
2011-11-21theories/, plugins/ and test-suite/ ported to the Arguments vernaculargareuselesinge
2011-11-21New Arguments vernaculargareuselesinge
2011-11-21Configurable simpl tacticgareuselesinge
2011-11-21Extend the computation of dependencies in pattern-matching compilationherbelin
2011-11-21Optimizing the compilation of unused aliases in pattern-matching.herbelin
2011-11-21Fixing postprocessing bugs in pattern-matching compilation.herbelin
2011-11-21Changed the way to detect if an "as" patterns is expanded or not. Theherbelin
2011-11-21Updating Cases.v test.herbelin
2011-11-17Fixing bug #2640 and variants of it (inconsistency between when andherbelin
2011-11-17Fixing new bug introduced in r14665 when fixing bug #1834.herbelin
2011-11-16Fixing bug #1834 (de Bruijn indices bug in pattern-matching compilation).herbelin
2011-11-16Suppression fichier Case8.v redondantherbelin
2011-11-08Improved check is_open_canonical_projectiongareuselesinge
2011-11-07Allow "|_=>_" in "match" in patterns, no more forced enumeration of constructorsletouzey
2011-11-06Fixing incorrect change to pattern-unification over Meta's introducedherbelin
2011-11-06Fixing tactic remember not correctly checking preservation of typingherbelin
2011-10-25Regression tests for bugs #2613 and #2616.herbelin
2011-10-25First attempt at making Print Assumption compatible with opaque modules (fix ...letouzey
2011-10-25Fixing "destruct" test.herbelin
2011-10-25New strategy to infer return predicate of match construct whenherbelin
2011-10-24Mod_subst: Attempt to fix #2608letouzey
2011-10-24Fixing another bug revealing ill-typed use of evar restriction.herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-28 00:04:04 +0000